theorem proved term proof

`nine_eq_8_plus_1`

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

formal statement (Lean)

 207theorem nine_eq_8_plus_1 : 9 = 8 + 1 := rfl

Term-mode proof.

 208
 209/-- Weak isospin I = 1/2 for doublets. -/

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use