apply_mem_rootsOfUnity — Mathlib

English

For unit a in R, χ(a) is a root of unity of order dividing |Rˣ|; i.e., χ(a) ∈ rootsOfUnity(|Rˣ|, R').

Русский

Для единицы a в R, χ(a) — корень единицы порядка, делящего |Rˣ|.

LaTeX

$$equivToUnitHom χ a ∈ rootsOfUnity (Fintype.card (Units R)) R'$$

Lean4

/-- The values of a multiplicative character on `R` are `n`th roots of unity, where `n = #Rˣ`. -/
theorem apply_mem_rootsOfUnity [Fintype Rˣ] (a : Rˣ) {χ : MulChar R R'} :
    equivToUnitHom χ a ∈ rootsOfUnity (Fintype.card Rˣ) R' := by
  rw [mem_rootsOfUnity, ← map_pow, ← (equivToUnitHom χ).map_one, pow_card_eq_one]

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