Theorems · Theorem · number theory

jacobiSum_eq_gaussSum_mul_gaussSum_div_gaussSum

∀ {F : Type u_1} {F' : Type u_2} [inst : Fintype F] [inst_1 : Field F] [inst_2 : Field F'],
  ↑(Fintype.card F) ≠ 0 →
    ∀ {χ φ : MulChar F F'},
      χ * φ ≠ 1 → ∀ {ψ : AddChar F F'}, ψ.IsPrimitive → jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ / gaussSum (χ * φ) ψ

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

Defined in

Mathlib.NumberTheory.JacobiSum.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeFieldField