exists_apply_eq_pow — Mathlib

English

Let χ be a multiplicative character with χ^n = 1, and μ a primitive root of unity of order n. Then for any a ≠ 0 there exists k < n with χ(a) = μ^k.

Русский

Пусть χ — мультипликативный характер с χ^n = 1 и μ — примитивный корень единства порядка n. Тогда для любого a ≠ 0 найдётся k < n such that χ(a) = μ^k.

LaTeX

$$$\forall {\chi : \mathrm{MulChar}(F,R)},\ (\chi^n = 1) \land (\text{IsPrimitiveRoot}(\mu,n)) \Rightarrow (\forall a \in F\setminus\{0\}, \exists k

Lean4

/-- If `χ` is a multiplicative character with `χ^n = 1` and `μ` is a primitive `n`th root
of unity, then, for `a ≠ 0`, there is some `k` such that `χ a = μ^k`. -/
theorem exists_apply_eq_pow {χ : MulChar F R} {n : ℕ} [NeZero n] (hχ : χ ^ n = 1) {μ : R} (hμ : IsPrimitiveRoot μ n)
    {a : F} (ha : a ≠ 0) : ∃ k < n, χ a = μ ^ k :=
  by
  obtain ⟨ζ, hζ₁, hζ₂⟩ := apply_mem_rootsOfUnity_of_pow_eq_one hχ ha
  have hζ' : ζ.val ^ n = 1 := (mem_rootsOfUnity' n ↑ζ).mp hζ₁
  obtain ⟨k, hk₁, hk₂⟩ := hμ.eq_pow_of_pow_eq_one hζ'
  exact ⟨k, hk₁, (hζ₂ ▸ hk₂).symm⟩

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