Complex Conjugate of an exponent

Stream: new members

[Shadman Sakib]

Hi, how would I find the complex conjugate of an exponent on Lean that is listed in the goal state as: ⇑conj (exp (2 * ↑π / ↑n * I)). In other words, what can I do to simplify this expression to simply exp(-(2 * ↑π / ↑n * I))?

[Yakov Pechersky]

import data.complex.exponential
import analysis.special_functions.trigonometric

open complex

notation `π` := real.pi

example (n : ℕ) :
  conj (exp (2 * π / n * I)) = exp (- (2 * π / n * I)) :=
begin
  norm_cast,
  rw [←exp_conj, conj.map_mul, conj_I, conj_of_real, neg_mul_eq_mul_neg]
end

[Yakov Pechersky]

Not sure why exp_conj is a simp lemma in the direction it is stated, one could make a case that it should be the simp in the other direction.

[Shadman Sakib]

Thanks!

[Yakov Pechersky]

Seems like there's a missing lemma:

import data.complex.exponential
import analysis.special_functions.trigonometric

@[simp] lemma complex.conj_inv (z : ℂ) :
  complex.conj z⁻¹ = (complex.conj z)⁻¹ :=
by { ext; simp [neg_div, neg_neg] }

open complex

notation `π` := real.pi

example (n : ℕ) :
  conj (exp (2 * π / n * I)) = exp (- (2 * π / n * I)) :=
begin
  norm_cast,
  simp [div_eq_mul_inv, ←exp_conj],
end

[Shadman Sakib]

Ahh yeah that fixes up a lot, code much more elegant

[Shadman Sakib]

Thanks

[Yakov Pechersky]

You don't even need the norm_cast then:

import data.complex.exponential
import analysis.special_functions.trigonometric

@[simp] lemma complex.conj_inv (z : ℂ) :
  complex.conj z⁻¹ = (complex.conj z)⁻¹ :=
by { ext; simp [neg_div, neg_neg] }

open complex

notation `π` := real.pi

example (n : ℕ) :
  conj (exp (2 * π / n * I)) = exp (- (2 * π / n * I)) :=
by simp [div_eq_mul_inv, ←exp_conj]

[Shadman Sakib]

Oh yeah haha, simp takes care of that. Good catch!

[Yakov Pechersky]

And of course, the complex.conj_inv is a specialization of a lemma that is true in any ring:

import data.complex.exponential
import analysis.special_functions.trigonometric

open complex

notation `π` := real.pi

example (n : ℕ) :
  conj (exp (2 * π / n * I)) = exp (- (2 * π / n * I)) :=
by simp [ring_hom.map_div, ←exp_conj]