apply_mem_algebraAdjoin — Mathlib

English

If χ is a multiplicative character with χ^n = 1 and μ is primitive root of order n, then χ(a) ∈ ℤ[μ] for all a ∈ F.

Русский

Если χ — мультипликативный характер с χ^n = 1 и μ — примитивный корень порядка n, то χ(a) ∈ ℤ[μ] для всех a ∈ F.

LaTeX

$$$\forall a ∈ F,\ χ(a) \in \mathbb{Z}[\mu],\ IsPrimitiveRoot(\mu,n).$$$

Lean4

/-- The values of a multiplicative character of order `n` are contained in `ℤ[μ]` when
`μ` is a primitive `n`th root of unity. -/
theorem apply_mem_algebraAdjoin {χ : MulChar F R} {μ : R} (hμ : IsPrimitiveRoot μ (orderOf χ)) (a : F) :
    χ a ∈ Algebra.adjoin ℤ { μ } :=
  have : NeZero (orderOf χ) := ⟨χ.orderOf_pos.ne'⟩
  apply_mem_algebraAdjoin_of_pow_eq_one (pow_orderOf_eq_one χ) hμ a

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