Theorem: RiemannSphere.coe_eq_zero (Ray/AnalyticManifold/RiemannSphere.lean)

State before:
z : ℂ
⊢ ↑z = 0 ↔ z = 0
Tactic:
simp only [← coe_zero, coe_eq_coe]
State after:
no goals