OAI/NumberTheory/Ostmann/Quadratic/QuadraticSmallCorrectionReindex.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The small-kernel conductor corrections use the actual shorter Jacobi matrices

  1. theorem OAI.Ostmann.quadraticGcdBlockCoeff_coprime line 12
  2. theorem OAI.Ostmann.quadratic_extra_weighted_reindex line 19
  3. theorem OAI.Ostmann.quadratic_gcd_small_correction_reindex line 83