OAI/NumberTheory/Ostmann/Construction/ExactGroupScalar.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Construction.primeSourceScalar line 13
2. def OAI.Ostmann.Construction.primeGroupScalar line 16
3. lemma OAI.Ostmann.Construction.balancedPrimeIndicator_nonneg line 20
4. theorem OAI.Ostmann.Construction.primeSourceScalar_nonneg line 26
5. theorem OAI.Ostmann.Construction.primeSourceScalar_balanced_lower line 30
6. theorem OAI.Ostmann.Construction.primeGroupScalar_nonneg line 43
7. theorem OAI.Ostmann.Construction.primeGroupScalar_lower line 50
8. theorem OAI.Ostmann.Construction.primeGroupScalar_exp_lower line 68
9. def OAI.Ostmann.Construction.nongiantScalar line 81
10. theorem OAI.Ostmann.Construction.nongiantScalar_exp_lower line 86