num * num_inv = 1

Stream: new members

[Shadman Sakib]

import tactic

example : (1 + (complex.I)) * (1 + complex.I)⁻¹ = 1 :=
begin

  sorry,
end

[Shadman Sakib]

how can I show this?

[Adam Topaz]

It's false if v = 1.

[Shadman Sakib]

How about this

[Shadman Sakib]

The #mwe is buggy, please give me one moment

[Adam Topaz]

import tactic
import data.complex.basic

example : (1 + (complex.I)) * (1 + complex.I)⁻¹ = 1 :=
mul_inv_cancel (λ c, by simpa using congr_arg complex.re c)

[Shadman Sakib]

Thank you, and sorry for the inconvenience

[Adam Topaz]

In general to prove lemmas such as a * a\inv = 1, you can to use docs#mul_inv_cancel but you need to produce a proof that a is nonzero.

[Adam Topaz]

If you have more complicated expressions, you can also use tactic#field_simp to clear denominators.

[Scott Morrison]

And a more general answer:

import tactic
import data.complex.basic

example : (1 + (complex.I)) * (1 + complex.I)⁻¹ = 1 :=
by suggest

produces a lot of rubbish, but amongst that rubbish is mul_inv_cancel, which hopefully you can guess from the name is what you're going to want.

[Scott Morrison]

and

import tactic
import data.complex.basic

example (z : ℂ) (h : z ≠ 0) : z * z⁻¹ = 1 :=
by library_search

just tells you the answer.