OAI/Combinatorics/SumProduct/Alignment/MalcevCentral01.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AbelianMalcevTorus.quotientHomeomorph_one line 28
  2. lemma OAI.AbelianMalcevTorus.quotientHomeomorph_mul line 32
  3. lemma OAI.AbelianMalcevTorus.quotientHomeomorph_symm_zero line 40
  4. lemma OAI.AbelianMalcevTorus.quotientHomeomorph_symm_add line 45
  5. def OAI.MalcevCentralTorus.addAction line 65
  6. lemma OAI.MalcevCentralTorus.continuous_addAction line 76
  7. lemma OAI.MalcevCentralTorus.torusProjection_vadd line 86
  8. lemma OAI.MalcevCentralTorus.invariant_addAction line 98
  9. lemma OAI.MalcevCentralTorus.central_commutative line 131
  10. lemma OAI.MalcevCentralTorus.central_lattice_normal line 136
  11. lemma OAI.MalcevCentralTorus.tail_additive line 144
  12. def OAI.MalcevCentralTorus.tailAction line 151
  13. lemma OAI.MalcevCentralTorus.continuous_tailAction line 156
  14. lemma OAI.MalcevCentralTorus.tailProjection_vadd line 163
  15. lemma OAI.MalcevCentralTorus.invariant_tailAction line 170
  16. lemma OAI.TorusVerticalFourier.character_norm line 190
  17. lemma OAI.TorusVerticalFourier.character_nontrivial line 193
  18. lemma OAI.TorusVerticalFourier.HasWeight.smul line 214
  19. theorem OAI.AbelianMalcevTorus.quantitative_abelian_compact_producer line 244