OAI/NumberTheory/Ostmann/Arithmetic/UnitResidueGrowth.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform square-root growth of the number of quadratic unit roots

  1. theorem OAI.Ostmann.exists_unit_residue_sqrt_bound line 10