OAI/GroupTheory/FiniteType/Representation.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Representation.coinvariantsLTensorEquiv line 16
  2. lemma OAI.Representation.coinvariantsLTensorEquiv_mk_tmul line 40
  3. def OAI.RelativeStandardFree.repEquiv line 51
  4. lemma OAI.RelativeStandardFree.repEquiv_apply line 54
  5. def OAI.RelativeStandardFree.freeCoinvariantEquiv line 57
  6. def OAI.RelativeStandardFree.coinvariantEquiv line 63
  7. lemma OAI.RelativeStandardFree.coinvariantEquiv_mk_tmul_single line 68
  8. def OAI.ListChains.standardProductEquiv line 85
  9. lemma OAI.ListChains.mapChain_relative_tuple line 91
  10. lemma OAI.ListChains.place_shifted_tuple line 100
  11. lemma OAI.ListChains.standardProductEquiv_mk_tmul_single line 115
  12. lemma OAI.ListChains.standardProductEquiv_mk_tmul line 130
  13. abbrev OAI.ControlledChains.Simplex line 152
  14. abbrev OAI.ControlledChains.Chain line 153
  15. def OAI.ControlledChains.boundary line 155
  16. lemma OAI.ControlledChains.boundary_single line 161
  17. lemma OAI.ControlledChains.boundary_boundary line 169
  18. def OAI.ControlledChains.mapChain line 183
  19. lemma OAI.ControlledChains.mapChain_single line 187
  20. lemma OAI.ControlledChains.boundary_mapChain line 193
  21. def OAI.ControlledChains.cone line 203
  22. lemma OAI.ControlledChains.cone_single line 207
  23. lemma OAI.ControlledChains.boundary_cone line 212
  24. def OAI.ControlledChains.augmentation line 237
  25. lemma OAI.ControlledChains.augmentation_single line 241
  26. lemma OAI.ControlledChains.boundary_cone_zero line 246
  27. lemma OAI.ControlledChains.augmentation_boundary line 267