pow_card_eq_one — Mathlib

English

The p-th power of a multiplicative character satisfies χ^(Fintype.card Mˣ) = 1.

Русский

Степень p = |Mˣ| такой, что χ^(|Mˣ|) = 1.

LaTeX

$$χ^(card(Mˣ)) = 1$$

Lean4

/-- If `χ` is a multiplicative character on a commutative monoid `M` with finitely many units,
then `χ ^ #Mˣ = 1`. -/
protected theorem pow_card_eq_one [Fintype Mˣ] (χ : MulChar M R) : χ ^ (Fintype.card Mˣ) = 1 :=
  by
  ext1
  rw [pow_apply_coe, ← map_pow, one_apply_coe, ← Units.val_pow_eq_pow_val, pow_card_eq_one, Units.val_eq_one.mpr rfl,
    map_one]

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