OAI/GroupTheory/FiniteType/InducedFree.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InducedFree.unit line 20
  2. def OAI.InducedFree.seed line 21
  3. def OAI.InducedFree.forward line 23
  4. def OAI.InducedFree.backward line 25
  5. lemma OAI.InducedFree.forward_mk line 28
  6. lemma OAI.InducedFree.seed_unit line 33
  7. lemma OAI.InducedFree.backward_unit line 35
  8. lemma OAI.InducedFree.backward_forward line 39
  9. lemma OAI.InducedFree.forward_backward line 46
  10. def OAI.InducedFree.iso line 55
  11. structure OAI.OrbitModule.Presentation line 65
  12. def OAI.OrbitModule.Presentation.ofIso line 77
  13. def OAI.OrbitModule.Presentation.induced line 90
  14. def OAI.OrbitModule.Presentation.ofBeginning line 114
  15. def OAI.ProductCoefficient.unitEquiv line 128
  16. lemma OAI.ProductCoefficient.unitEquiv_comm line 130
  17. def OAI.ProductCoefficient.unitIso line 143
  18. def OAI.ListChains.flattenProduct line 149
  19. lemma OAI.ListChains.flatten_bounded line 151
  20. lemma OAI.ListChains.flatten_degree line 156
  21. lemma OAI.ListChains.flatten_boundary line 160
  22. def OAI.ListChains.gatherProduct line 166
  23. lemma OAI.ListChains.gather_apply line 169
  24. lemma OAI.ListChains.gather_bounded line 173
  25. lemma OAI.ListChains.gather_degree line 183
  26. lemma OAI.ListChains.gather_boundary line 192
  27. lemma OAI.ListChains.gather_flatten line 201
  28. lemma OAI.ListChains.bounded_filling_unit line 212
  29. theorem OAI.ListChains.productCoefficient_vanishing line 226