Complex Conjugate of a natural number

Stream: new members

[Shadman Sakib]

import analysis.complex.circle
import analysis.special_functions.trigonometric
import group_theory.specific_groups.dihedral
noncomputable theory

open complex dihedral_group
lemma conj_nat (k : ℕ) : conj(k) = k :=
begin
  sorry,
end

[Shadman Sakib]

Since there exists a conj_of_real theorem, how can I cast the k to a real so I can apply conj_of_real? Or is there another way than casting?

[Kevin Buzzard]

I get an unknown identifier conj error in your code. Can you supply a #mwe ?

[Shadman Sakib]

Does that work?

[Eric Wieser]

I think you want docs#ring_hom.map_nat_cast

[Shadman Sakib]

Ahh thank you!

[Eric Wieser]

Note that you could have just asked lean this rather than asking a human:

import data.complex.basic

open complex

lemma conj_nat (k : ℕ) : conj k = k :=
begin
  simp?,
end