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

State before:
⊢ OnePoint.toComplex 0 = 0
Tactic:
rw [← coe_zero, toComplex_coe]
State after:
no goals