English
If χ^n = φ^n = 1 and μ is a primitive nth root of unity in R, then J(χ, φ) ∈ ℤ[μ] ⊆ R.
Русский
Если χ^n = φ^n = 1 и μ — примитивный корень μ-го единичного корня, то J(χ, φ) ∈ ℤ[μ] ⊆ R.
LaTeX
$$$$ \mathrm{jacobiSum}(χ, φ) \in \mathbb{Z}[\mu] \subseteq R, \quad χ^n = φ^n = 1, \; μ \text{ primitive of } n. $$$$
Lean4
/-- If `χ` and `φ` are multiplicative characters on a finite field `F` satisfying `χ^n = φ^n = 1`
and with values in an integral domain `R`, and `μ` is a primitive `n`th root of unity in `R`,
then the Jacobi sum `J(χ,φ)` is in `ℤ[μ] ⊆ R`. -/
theorem jacobiSum_mem_algebraAdjoin_of_pow_eq_one {n : ℕ} [NeZero n] {χ φ : MulChar F R} (hχ : χ ^ n = 1)
(hφ : φ ^ n = 1) {μ : R} (hμ : IsPrimitiveRoot μ n) : jacobiSum χ φ ∈ Algebra.adjoin ℤ { μ } :=
Subalgebra.sum_mem _ fun _ _ ↦
Subalgebra.mul_mem _ (MulChar.apply_mem_algebraAdjoin_of_pow_eq_one hχ hμ _)
(MulChar.apply_mem_algebraAdjoin_of_pow_eq_one hφ hμ _)
