Theorems · Theorem · number theory

jacobiSum_mul_jacobiSum_inv

∀ {F : Type u_1} {F' : Type u_2} [inst : Fintype F] [inst_1 : Field F] [inst_2 : Field F'],
  ringChar F' ≠ ringChar F →
    ∀ {χ φ : MulChar F F'}, χ ≠ 1 → φ ≠ 1 → χ * φ ≠ 1 → jacobiSum χ φ * jacobiSum χ⁻¹ φ⁻¹ = ↑(Fintype.card F)

If χ and φ are multiplicative characters on a finite field F with values in another field F' such that χ, φ and χφ are all nontrivial and char F' ≠ char F, then J(χ,φ) * J(χ⁻¹,φ⁻¹) = #F (in F').

Defined in

Mathlib.NumberTheory.JacobiSum.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeFieldField