OAI/NumberTheory/CubicMoment/Estimates/SmallBRealLength.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integer norms permit an exact floor cutoff after division by a common factor. No rounding error is added to the coefficient support.

  1. theorem OAI.CubicFirstMoment.smallB_coprime_height_real line 11