## Stream: new members

### Topic: num * num_inv = 1

#### Shadman Sakib (Aug 26 2021 at 18:48):

import tactic

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

sorry,
end


#### Shadman Sakib (Aug 26 2021 at 18:48):

how can I show this?

#### Adam Topaz (Aug 26 2021 at 18:49):

It's false if v = 1.

How about this

#### Shadman Sakib (Aug 26 2021 at 19:12):

The #mwe is buggy, please give me one moment

#### Adam Topaz (Aug 26 2021 at 19:13):

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 (Aug 26 2021 at 19:14):

Thank you, and sorry for the inconvenience

#### Adam Topaz (Aug 26 2021 at 19:14):

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 (Aug 26 2021 at 19:15):

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

#### Scott Morrison (Aug 27 2021 at 00:56):

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 (Aug 27 2021 at 01:00):

and

import tactic
import data.complex.basic

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


just tells you the answer.

Last updated: Dec 20 2023 at 11:08 UTC