ring.inverse equals has_inv.inv

Stream: Is there code for X?

[Eric Wieser]

Do we have this anywhere?

example {G₀} [group_with_zero G₀] (g : G₀) : ring.inverse g = g⁻¹ :=
begin
  obtain rfl | hg := eq_or_ne g 0,
  { rw [ring.inverse_non_unit (0 : G₀) (not_is_unit_zero), _root_.inv_zero], },
  { lift g to units G₀ using hg,
    rw [ring.inverse_unit, units.coe_inv'] }
end

[Eric Wieser]

Ah, its docs#inverse_eq_has_inv which has bad assumptios and a bad namespace

[Eric Wieser]

#10033 to rename it to start with ring.