OAI/NumberTheory/Ostmann/Arithmetic/ResidueHaar.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.ResidueHaar.average line 9
2. theorem OAI.Ostmann.Arithmetic.ResidueHaar.average_equiv line 12
3. theorem OAI.Ostmann.Arithmetic.ResidueHaar.average_product line 17
4. def OAI.Ostmann.Arithmetic.ResidueHaar.crtUnits line 24
5. theorem OAI.Ostmann.Arithmetic.ResidueHaar.crt_average_product line 28
6. def OAI.Ostmann.Arithmetic.ResidueHaar.splitEquiv line 35
7. theorem OAI.Ostmann.Arithmetic.ResidueHaar.split_average line 41
8. def OAI.Ostmann.Arithmetic.ResidueHaar.fixedProductEquiv line 46
9. theorem OAI.Ostmann.Arithmetic.ResidueHaar.fixedProduct_card line 61