OAI/GroupTheory/Hyperbolic/CyclicAction.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Release075.FreeChain.shift_apply line 10
  2. theorem OAI.Release075.FreeChain.shift_one line 14
  3. theorem OAI.Release075.FreeChain.shift_mul line 17
  4. abbrev OAI.Release075.FreeChain.RightCosets line 21
  5. def OAI.Release075.FreeChain.coset line 23
  6. def OAI.Release075.FreeChain.cosetCoord line 25
  7. theorem OAI.Release075.FreeChain.coset_mul line 29
  8. def OAI.Release075.FreeChain.rightCosetEquiv line 36
  9. def OAI.Release075.FreeChain.chainCosetEquiv line 49
  10. theorem OAI.Release075.FreeChain.chainCosetEquiv_coeff line 56
  11. theorem OAI.Release075.FreeChain.chainCosetEquiv_shift line 61
  12. def OAI.Release075.FreeChain.subgroupNorm line 71
  13. theorem OAI.Release075.FreeChain.chainCosetEquiv_norm line 74
  14. theorem OAI.Release075.finsupp_preimages line 91
  15. theorem OAI.Release075.regular_invariant_norm line 104
  16. theorem OAI.Release075.regular_norm_zero line 114
  17. theorem OAI.Release075.FreeChain.invariant_is_norm line 128
  18. theorem OAI.Release075.FreeChain.norm_zero_is_difference line 143
  19. def OAI.Release075.FreeChain.augmentation line 165
  20. theorem OAI.Release075.FreeChain.augmentation_single line 169
  21. theorem OAI.Release075.FreeChain.augmentation_shift line 173
  22. theorem OAI.Release075.FreeChain.norm_map line 181
  23. theorem OAI.Release075.FreeChain.augmentation_norm line 188
  24. theorem OAI.Release075.FreeChain.cyclic_chain_obstruction line 192