Theorem: RiemannSphere.inv_zero' (Ray/AnalyticManifold/RiemannSphere.lean)

State before:
⊢ 0⁻¹ = ∞
Tactic:
simp only [inv_def, inv, eq_self_iff_true, if_true]
State after:
no goals