English
The complex conjugation sends a torsion unit to its inverse within the units of the ring of integers.
Русский
Сопряжение отправляетtorsion-единицу в её обратную, внутри группы единиц кольца целых.
LaTeX
$$$$ complexConj_K(\\zeta)=\\zeta^{-1} \\quad \\text{for all } \\zeta \\in \\mathrm{torsion}(K). $$$$
Lean4
/-- The image of a root of unity by the complex conjugation is its inverse.
This is the version of `Complex.conj_rootsOfUnity` for CM-fields.
-/
@[simp]
theorem complexConj_torsion (ζ : torsion K) : complexConj K (ζ.val : K) = (ζ.val : K)⁻¹ :=
by
let φ : K →+* ℂ := Classical.choice (inferInstance : Nonempty _)
apply φ.injective
rw [complexEmbedding_complexConj, ← Units.complexEmbedding_apply, Complex.conj_rootsOfUnity (n := torsionOrder K),
Units.val_inv_eq_inv_val, Units.complexEmbedding_apply, map_inv₀]
exact map_complexEmbedding_torsion K φ ▸ Subgroup.apply_coe_mem_map _ _ _
