# Zulip Chat Archive

## 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