English
If χ^n = 1 for some n and a ≠ 0, then χ(a) is an nth root of unity; explicitly there exists ζ ∈ rootsOfUnity(n,R) with χ(a) = ζ.
Русский
Если χ^n = 1 и a ≠ 0, то χ(a) является корнем единства порядка n; существует ζ ∈ rootsOfUnity(n,R) такой, что χ(a) = ζ.
LaTeX
$$$\forall {\chi : \mathrm{MulChar}(F,R)}\ \forall {n:\mathbb{N}}, (\chi^n = 1) \Rightarrow (\forall a \in F\setminus\{0\}, \exists \zeta \in \mathrm{rootsOfUnity}(n,R), \chi(a) = \zeta).$$$
Lean4
/-- The non-zero values of a multiplicative character `χ` such that `χ^n = 1`
are `n`th roots of unity. -/
theorem apply_mem_rootsOfUnity_of_pow_eq_one {χ : MulChar F R} {n : ℕ} (hχ : χ ^ n = 1) {a : F} (ha : a ≠ 0) :
∃ ζ ∈ rootsOfUnity n R, ζ = χ a :=
by
obtain ⟨μ, hμ₁, hμ₂⟩ := χ.apply_mem_rootsOfUnity_orderOf ha
exact
⟨μ, rootsOfUnity_le_of_dvd (orderOf_dvd_of_pow_eq_one hχ) hμ₁, hμ₂⟩
-- Results involving primitive roots of unity require `R` to be an integral domain.
