OAI/NumberTheory/DukePrimeDegree/Geometry/QuantitativeQuotientCover.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite quotient covers with quantitative size control

Entrywise grids of bounded representatives give open covers of the logarithmic quotient balls. Each member has uniformly small relative lifts, and the number of members has an explicit grid bound.

  1. theorem OAI.DukePrimeDegree.exists_quantitative_quotient_cover line 19