Theorems · Theorem · number theory

Char.card_pow_char_pow

∀ {R : Type u} [inst : CommRing R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] [IsDomain R']
  {χ : MulChar R R'},
  χ.IsQuadratic →
    ∀ (ψ : AddChar R R') (p n : ℕ) [fp : Fact (Nat.Prime p)] [hch : CharP R' p],
      IsUnit ↑p →
        p ≠ 2 → gaussSum χ ψ ^ 2 = χ (-1) * ↑(Fintype.card R) → (χ (-1) * ↑(Fintype.card R)) ^ (p ^ n / 2) = χ (↑p ^ n)

If the square of the Gauss sum of a quadratic character is χ(-1) * #R, then we get, for all n : ℕ, the relation (χ(-1) * #R) ^ (p^n/2) = χ(p^n), where p is the (odd) characteristic of the target ring R'. This version can be used when R is not a field, e.g., ℤ/8ℤ.

Defined in

Mathlib.NumberTheory.GaussSum

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingFintypeCommRingIsDomainFactCharP