OAI/Combinatorics/SumProduct/Alignment/AbelianMalcev02.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AbelianMalcevTorus.metricHomeomorph line 32
2. lemma OAI.AbelianMalcevTorus.metricHomeomorph_apply line 42
3. lemma OAI.AbelianMalcevTorus.metric_compact line 47
4. lemma OAI.AbelianMalcevTorus.metric_borelSpace line 55
5. theorem OAI.AbelianMalcevTorus.metric_coordinateHaar_map line 60
6. def OAI.AbelianMalcevTorus.additiveCoordinates line 86
7. abbrev OAI.AbelianMalcevTorus.integerCharacter line 92
8. lemma OAI.AbelianMalcevTorus.integerCharacter_apply line 96
9. lemma OAI.AbelianMalcevTorus.basis_integerCharacter line 99
10. theorem OAI.AbelianMalcevTorus.polynomial_coordinates line 109
11. lemma OAI.AbelianMalcevTorus.coordinates_additive_of_commutator_bot line 121
12. lemma OAI.AbelianMalcevTorus.coordinates_additive_of_secondLevel_bot line 130
13. theorem OAI.TorusLeibman.quantitative_homeomorphic_torus line 153
14. theorem OAI.AbelianMalcevTorus.quantitative_abelian_producer line 208