def definition def or abbrev

`M0`

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

formal statement (Lean)

 100def M0 : ℝ := 1

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

QuarkAbsoluteMassResidual in IndisputableMonolith.Masses.QuarkScoreCard decl_use
anchor_ratio in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
M0 in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
M0_pos in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
massAtAnchor in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
AnchorCert in IndisputableMonolith.Recognition.Certification decl_use
M0_pos_of_cert in IndisputableMonolith.Recognition.Certification decl_use
Valid in IndisputableMonolith.Recognition.Certification decl_use
zeroWidthCert in IndisputableMonolith.Recognition.Certification decl_use
anchor_ratio in IndisputableMonolith.RSBridge.Anchor decl_use
M0_pos in IndisputableMonolith.RSBridge.Anchor decl_use
massAtAnchor in IndisputableMonolith.RSBridge.Anchor decl_use

Lean names referenced from this declaration's body.