## Stream: maths

### Topic: conj_mul_eq_abs_sq_left

#### François Sunatori (Mar 11 2021 at 00:41):

Hi,
I'm trying to prove the following lemma:

import analysis.complex.basic
import data.complex.is_R_or_C

open complex

local notation | x | := complex.abs x

lemma conj_mul_eq_abs_sq_left (z : ℂ) : conj z * z = |z| ^ 2 :=
begin
sorry
end


and found  is_R_or_C.conj_mul_eq_norm_sq_left which is defined as x† * x = ((norm_sq x) : K)
but I'm unsure how to change conj into † when trying to do rw is_R_or_C.conj_mul_eq_norm_sq_left z.
Is there a way to change a ℂ to a is_R_or_C?
Thank you!

#### Heather Macbeth (Mar 11 2021 at 00:51):

On the one hand, yes, we have docs#complex.is_R_or_C, so lemmas about is_R_or_C apply to ℂ. On the other hand, usually a lemma about is_R_or_C will have a parallel version for ℂ itself which we use preferentially (because otherwise it can get confusing switching between one and the other within the same proof).

So, use docs#complex.norm_sq_eq_conj_mul_self, not the is_R_or_C version!

#### François Sunatori (Mar 11 2021 at 00:53):

Oh cool, I hadn't seen that one. Ok I'll stick to ℂ then. Thank you :)

Last updated: May 10 2021 at 06:13 UTC