Zulip Chat Archive

Stream: new members

Topic: Complex Conjugate of a natural number

Shadman Sakib (Jul 11 2021 at 15:28):

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

Shadman Sakib (Jul 11 2021 at 15:30):

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 (Jul 11 2021 at 15:32):

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

Shadman Sakib (Jul 11 2021 at 15:33):

Does that work?

Eric Wieser (Jul 11 2021 at 15:34):

I think you want docs#ring_hom.map_nat_cast

Shadman Sakib (Jul 11 2021 at 15:36):

Ahh thank you!

Eric Wieser (Jul 11 2021 at 15:38):

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

Last updated: Dec 20 2023 at 11:08 UTC