theorem proved wrapper

`M0_pos`

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

formal statement (Lean)

 101@[simp] theorem M0_pos : 0 < M0 := by

One-line wrapper that applies dsimp.

 102  dsimp [M0]; norm_num
 103

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

heavy_anchor_positive in IndisputableMonolith.Masses.QuarkAnchorDerivation decl_use
M0_pos_of_cert in IndisputableMonolith.Recognition.Certification decl_use
Valid in IndisputableMonolith.Recognition.Certification decl_use
zeroWidthCert_valid in IndisputableMonolith.Recognition.Certification decl_use
M0_pos in IndisputableMonolith.RSBridge.Anchor decl_use

Lean names referenced from this declaration's body.