OAI/NumberTheory/Ostmann/Quadratic/QuadraticUnitDivisor.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The divisor-one block, retained separately from positive dyadic intervals

  1. theorem OAI.Ostmann.quadratic_unit_divisor_bound line 11
  2. theorem OAI.Ostmann.quadratic_gauss_unit_divisor_bound line 37