Zulip Chat Archive

Stream: maths

Topic: conj_mul_eq_abs_sq_left

view this post on Zulip François Sunatori (Mar 11 2021 at 00:41):

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 :=

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!

view this post on Zulip 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!

view this post on Zulip 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