Theorems · Theorem · number theory

quadraticChar_odd_prime

∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
  ringChar F ≠ 2 →
    ∀ {p : ℕ} [inst_3 : Fact (Nat.Prime p)],
      p ≠ 2 →
        ringChar F ≠ p →
          (quadraticChar F) ↑p = (quadraticChar (ZMod p)) (↑(ZMod.χ₄ ↑(Fintype.card F)) * ↑(Fintype.card F))

The value of the quadratic character at an odd prime p different from ringChar F.

Defined in: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum
Cited by: 2 results in Mathlib
Foundations: Depth 223 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field Fintype DecidableEq Fact

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites16

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Fintypestatement and proof · cited by 7,736
Fieldstatement and proof · cited by 7,404
Factstatement and proof · cited by 2,726
Nat.Primestatement and proof · cited by 2,059
Fintype.cardstatement and proof · cited by 1,386
ZModstatement and proof · cited by 1,024
MulCharstatement · cited by 186
ringCharstatement and proof · cited by 73
ZMod.cardproof · cited by 36
quadraticCharstatement and proof · cited by 34
ZMod.χ₄statement · cited by 27

Cited by2

Results whose statement or proof uses this declaration.

legendreSym.quadratic_reciprocityproof · cited by 1
FiniteField.isSquare_odd_prime_iffproof · cited by 0