Problem with mul_inv_eq_one

Stream: new members

[Luke Mantle]

I'm using mul_inv_eq_one in a larger proof but I can't seem to get it to work even in this very basic example:

import analysis.analytic.basic
open real

example (a : ℝ) : a * a⁻¹ = 1 :=
begin
  apply mul_inv_eq_one.mpr,
end

[Jireh Loreaux]

you need docs#mul_inv_eq_one₀ because ℝ isn't a group, it's a docs#group_with_zero.

[Jireh Loreaux]

And a hypothesis (ha : a ≠ 0).

[Luke Mantle]

Jireh Loreaux said:

you need docs#mul_inv_eq_one₀ because ℝ isn't a group, it's a docs#group_with_zero.

Ah, ok. Thanks!