OAI/NumberTheory/Ostmann/QuadraticCenter/PrimeQuadraticUniqueness.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The only nonprincipal quadratic character at a prime

  1. def OAI.Ostmann.complexJacobiCharacter line 9
  2. theorem OAI.Ostmann.prime_character_eq_of_square_eq_one line 12
  3. theorem OAI.Ostmann.complexJacobiCharacter_square line 34
  4. theorem OAI.Ostmann.complexJacobiCharacter_ne_one line 41
  5. theorem OAI.Ostmann.prime_quadratic_character_unique line 54