absolute value and complex conjugate

Stream: Is there code for X?

[Jeremy Avigad]

I am confused about the right way to use absolute value and complex conjugate on the complex numbers. I need (some incarnation of) the inference below, but the proof I found seems messy and roundabout. Can someone tell me if there is a better way?

import data.complex.basic

open complex
open_locale complex_conjugate

example (z w : complex) (h : abs z = abs w) : z * star z = w * star w :=
begin
  transitivity ((complex.abs z ^ 2 : ℝ) : ℂ),
  { rw [complex.sq_abs, ←complex.mul_conj], refl },
  transitivity ((complex.abs w ^ 2 : ℝ) : ℂ),
  { rw h },
  rw [complex.sq_abs, ←complex.mul_conj], refl
end

[Eric Rodriguez]

one solution that people may frown upon a little would be this:

example (z w : complex) (h : abs z = abs w) : z * star z = w * star w :=
by simpa [complex.mul_conj] using (real.sqrt_inj _ _).mp h; apply norm_sq_nonneg

[Eric Rodriguez]

this is a bit brittle against API change though

[Anatole Dedecker]

I would do

example (z w : complex) (h : abs z = abs w) : z * star z = w * star w :=
by rw [← star_ring_end_apply, complex.mul_conj, ← star_ring_end_apply, complex.mul_conj,
  norm_sq_eq_abs, norm_sq_eq_abs, h]

[Eric Rodriguez]

one that's less hacky: simpa [complex.sq_abs, complex.mul_conj] using congr_arg (^ 2) h,

[Anatole Dedecker]

Yes invoking injectivity of square root seems wrong

[Heather Macbeth]

By the way, I think we prefer conj over star (in order to sound more like what outsiders expect); open_locale complex_conjugate precisely enables the conj notation.

[Moritz Doll]

using conj also makes it possible to golf Anatole's proof to simp_rw [mul_conj, complex.norm_sq_eq_abs, h]

[Anatole Dedecker]

I have this habit of trying rw before simp and I can't decide if it's good or not :sweat_smile:

[Jeremy Avigad]

Thank you!