conj_rootsOfUnity — Mathlib

English

For ζ ∈ rootsOfUnity n ℂˣ one has the complex conjugation acting as inverse: conjugate(ζ) = ζ⁻¹.

Русский

Для ζ ∈ rootsOfUnity n ℂˣ сопряжение действует как обратное: ζ̄ = ζ⁻¹.

LaTeX

$$Complex.conj_rootsOfUnity: hζ ∈ rootsOfUnity n ℂˣ → (starRingEnd ℂ) ζ = ζ⁻¹$$

Lean4

theorem conj_rootsOfUnity {ζ : ℂˣ} {n : ℕ} [NeZero n] (hζ : ζ ∈ rootsOfUnity n ℂ) : (starRingEnd ℂ) ζ = ζ⁻¹ := by
  rw [← Units.mul_eq_one_iff_eq_inv, conj_mul', norm_eq_one_of_mem_rootsOfUnity hζ, ofReal_one, one_pow]

Похожие утверждения