pith. machine review for the scientific record. sign in
theorem proved term proof

ZOf_charged_leptons

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  53theorem ZOf_charged_leptons : ZOf .e = 1332 ∧ ZOf .mu = 1332 ∧ ZOf .tau = 1332 := by

proof body

Term-mode proof.

  54  refine ⟨?_, ?_, ?_⟩ <;> · decide
  55
  56/-! ## Equal-Z within a sector implies pure φ-power ratios -/
  57

used by (1)

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

depends on (7)

Lean names referenced from this declaration's body.