Theorems · Theorem · number theory

quadraticChar_card_card

∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F],
  ringChar F ≠ 2 →
    ∀ {F' : Type u_2} [inst_3 : Field F'] [inst_4 : Fintype F'] [inst_5 : DecidableEq F'],
      ringChar F' ≠ 2 →
        ringChar F' ≠ ringChar F →
          (quadraticChar F) ↑(Fintype.card F') = (quadraticChar F') (↑((quadraticChar F) (-1)) * ↑(Fintype.card F))

The relation between the values of the quadratic character of one field F at the cardinality of another field F' and of the quadratic character of F' at the cardinality of F.

Defined in

Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFintypeDecidableEqFieldFintypeDecidableEq