lemma
proved
term proof
zero
show as:
view Lean formalization →
formal statement (Lean)
68lemma zero (φ : ℝ) : PhiClosed φ (0 : ℝ) :=
proof body
Term-mode proof.
69 (phiSubfield φ).zero_mem
70