conj_mul_eq_abs_sq_left

Stream: maths

[François Sunatori]

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]

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]

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