def definition def or abbrev

`c_coercive`

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

formal statement (Lean)

  34def c_coercive : ℚ := 49 / 162

Definition body.

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

c_coercive_approx in IndisputableMonolith.Gravity.CoerciveProjection decl_use
c_coercive_pos in IndisputableMonolith.Gravity.CoerciveProjection decl_use
c_coercive_value in IndisputableMonolith.Gravity.CoerciveProjection decl_use
CoerciveProjectionCert in IndisputableMonolith.Gravity.CoerciveProjection decl_use