theorem
proved
term proof
phi_psi_sum
show as:
view Lean formalization →
formal statement (Lean)
101theorem phi_psi_sum : φ + ψ = 1 := by
proof body
Term-mode proof.
102 unfold φ ψ; ring
103
104/-- **THEOREM: φ − ψ = √5** -/