OAI/NumberTheory/DirichletL/Descent/GlobalPrincipalMass.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SevenEighths.InverseMomentGlobalPrincipalMass.Core line 15
2. def OAI.SevenEighths.InverseMomentGlobalPrincipalMass.core line 17
3. def OAI.SevenEighths.InverseMomentGlobalPrincipalMass.divisorTarget line 20
4. lemma OAI.SevenEighths.InverseMomentGlobalPrincipalMass.divisorTarget_ne_zero line 23
5. lemma OAI.SevenEighths.InverseMomentGlobalPrincipalMass.firstDivisor_dvd_target line 28
6. theorem OAI.SevenEighths.InverseMomentGlobalPrincipalMass.core_fiber_card line 39
7. theorem OAI.SevenEighths.InverseMomentGlobalPrincipalMass.core_fiber_small_power line 69
8. lemma OAI.SevenEighths.InverseMomentGlobalPrincipalMass.divisorTarget_norm_bound line 94