Theorems · Theorem · number theory

jacobiSum_mul_nontrivial

∀ {F : Type u_1} {R : Type u_2} [inst : Field F] [inst_1 : Fintype F] [inst_2 : CommRing R] [IsDomain R]
  {χ φ : MulChar F R}, χ * φ ≠ 1 → ∀ (ψ : AddChar F R), gaussSum (χ * φ) ψ * jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ

If χ and φ are multiplicative characters on a finite field F such that χφ is nontrivial, then g(χφ) * J(χ,φ) = g(χ) * g(φ).

Defined in

Mathlib.NumberTheory.JacobiSum.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldFintypeCommRingIsDomain