OAI/NumberTheory/Ostmann/Arithmetic/ArithmeticQuadraticCoefficient.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Dependence of the original coefficient on finite arithmetic residues

  1. def OAI.Ostmann.quadraticInverseResidue line 12
  2. def OAI.Ostmann.quadraticSymbolCoefficient line 15
  3. def OAI.Ostmann.quadraticDivisorSymbol line 18
  4. def OAI.Ostmann.arithmeticQuadraticCoefficient line 21
  5. theorem OAI.Ostmann.quadraticSymbolCoefficient_norm_le line 27
  6. theorem OAI.Ostmann.quadraticDivisorSymbol_norm_le line 34
  7. theorem OAI.Ostmann.realJacobi_mod_multiple line 39
  8. theorem OAI.Ostmann.quadraticInverseResidue_mod_multiple line 46
  9. theorem OAI.Ostmann.primeDivisorPositive_congr_point line 55
  10. theorem OAI.Ostmann.fullQuadraticCoefficient_congr_on line 67
  11. theorem OAI.Ostmann.arithmeticQuadraticCoefficient_mod line 90