theorem
proved
term proof
primeCounting_zero
show as:
view Lean formalization →
formal statement (Lean)
354theorem primeCounting_zero : primeCounting 0 = 0 := by
proof body
Term-mode proof.
355 simp [primeCounting]
356
357/-- π(1) = 0. -/