OAI/NumberTheory/Ostmann/Construction/RegularGiantMultiplier.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The displayed regular-prime multiplier on actual natural giants

  1. def OAI.Ostmann.naturalRegularMultiplier line 11
  2. def OAI.Ostmann.guardedRegularMultiplier line 17
  3. theorem OAI.Ostmann.guardedRegularMultiplier_modEq line 23
  4. theorem OAI.Ostmann.guardedRegularMultiplier_eq_diagonal line 34
  5. theorem OAI.Ostmann.guardedRegularMultiplier_bound line 47
  6. theorem OAI.Ostmann.movingNaturalGiantUnits_root line 69
  7. theorem OAI.Ostmann.movingSupportedWeight_regular_multiplier line 76