theorem proved term proof

`c_eq_one`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 102theorem c_eq_one : c = 1 := by rfl

Term-mode proof.

 103
 104/-- **CALCULATED**: c > 0. -/

From the project-wide theorem graph. These declarations reference this one in their body.

ConstantsPredictionsCert in IndisputableMonolith.Unification.ConstantsPredictionsProved decl_use
constants_predictions_cert_exists in IndisputableMonolith.Unification.ConstantsPredictionsProved decl_use
c_positive in IndisputableMonolith.Unification.ConstantsPredictionsProved decl_use