Theorems · Theorem · number theory

jacobiSum_mem_algebraAdjoin_of_pow_eq_one

∀ {F : Type u_1} {R : Type u_2} [inst : Field F] [inst_1 : CommRing R] [IsDomain R] [inst_3 : Fintype F] {n : ℕ}
  [NeZero n] {χ φ : MulChar F R}, χ ^ n = 1 → φ ^ n = 1 → ∀ {μ : R}, IsPrimitiveRoot μ n → jacobiSum χ φ ∈ ℤ[μ]

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 nth root of unity in R, then the Jacobi sum J(χ,φ) is in ℤ[μ] ⊆ R.

Defined in

Mathlib.NumberTheory.JacobiSum.Basic

Cited by

0 results in Mathlib

Foundations

Depth 143 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldCommRingIsDomainFintypeNeZero