English
For a multiplicative character χ on F with a nonzero argument a ∈ F×, the value χ(a) is a root of unity of order equal to the order of χ. Equivalently, χ(a) lies in the group of nth roots of unity where n = order(χ).
Русский
Для мультиchar χ на F и невыходного аргумента a ∈ F× значение χ(a) является корнем единства порядка order(χ). Иначе говоря, χ(a) принадлежит множеству корней единства порядка n = order(χ).
LaTeX
$$$\forall \chi \in \mathrm{MulChar}(F,R),\ \forall a \in F^{\times},\ \exists \zeta \in \mathrm{rootsOfUnity}(\operatorname{order}(\chi))\, (\zeta = \chi(a)).$$$
Lean4
theorem apply_mem_rootsOfUnity_orderOf (χ : MulChar F R) {a : F} (ha : a ≠ 0) :
∃ ζ ∈ rootsOfUnity (orderOf χ) R, ζ = χ a :=
by
have hu : IsUnit (χ a) := ha.isUnit.map χ
refine ⟨hu.unit, ?_, hu.unit_spec⟩
rw [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val, Units.val_one, IsUnit.unit_spec, ←
χ.pow_apply' χ.orderOf_pos.ne', pow_orderOf_eq_one,
show a = (isUnit_iff_ne_zero.mpr ha).unit by simp only [IsUnit.unit_spec], MulChar.one_apply_coe]
