English
If χ^n = 1 and μ is a primitive nth root of unity, then for any a ∈ F, the value χ(a) lies in the ring ℤ[μ].
Русский
Если χ^n = 1 и μ — примитивный корень единства порядка n, то для любого a ∈ F значение χ(a) принадлежит кольцу ℤ[μ].
LaTeX
$$$\forall a ∈ F,\ χ(a) ∈ \mathbb{Z}[\mu]$ when χ^n = 1 and μ^n = 1 with μ primitive.$$
Lean4
/-- The values of a multiplicative character `χ` such that `χ^n = 1` are contained in `ℤ[μ]` when
`μ` is a primitive `n`th root of unity. -/
theorem apply_mem_algebraAdjoin_of_pow_eq_one {χ : MulChar F R} {n : ℕ} [NeZero n] (hχ : χ ^ n = 1) {μ : R}
(hμ : IsPrimitiveRoot μ n) (a : F) : χ a ∈ Algebra.adjoin ℤ { μ } :=
by
rcases eq_or_ne a 0 with rfl | h
· exact χ.map_zero ▸ Subalgebra.zero_mem _
· obtain ⟨ζ, hζ₁, hζ₂⟩ := apply_mem_rootsOfUnity_of_pow_eq_one hχ h
rw [mem_rootsOfUnity, Units.ext_iff, Units.val_pow_eq_pow_val] at hζ₁
obtain ⟨k, _, hk⟩ := IsPrimitiveRoot.eq_pow_of_pow_eq_one hμ hζ₁
exact hζ₂ ▸ hk ▸ Subalgebra.pow_mem _ (Algebra.self_mem_adjoin_singleton ℤ μ) k
