theorem
proved
term proof
Z_lepton_decomposition
show as:
view Lean formalization →
formal statement (Lean)
84theorem Z_lepton_decomposition :
85 (1 : ℤ) * (-6) ^ 2 = 36 ∧
86 (1 : ℤ) * (-6) ^ 4 = 1296 ∧
87 (36 : ℤ) + 1296 = 1332 := by
proof body
Term-mode proof.
88 refine ⟨by norm_num, by norm_num, by norm_num⟩
89
90/-- Consistency: the derived Z equals 1332, matching Anchor.lean's hardcoded value. -/