Theorems · Theorem · number theory

Char.card_pow_card

∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] {F' : Type u_2} [inst_2 : Field F'] [inst_3 : Fintype F']
  {χ : MulChar F F'},
  χ ≠ 1 →
    χ.IsQuadratic →
      ringChar F' ≠ ringChar F →
        ringChar F' ≠ 2 → (χ (-1) * ↑(Fintype.card F)) ^ (Fintype.card F' / 2) = χ ↑(Fintype.card F')

When F and F' are finite fields and χ : F → F' is a nontrivial quadratic character, then (χ(-1) * #F)^(#F'/2) = χ #F'.

Defined in

Mathlib.NumberTheory.GaussSum

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFintypeFieldFintype