OAI/GroupTheory/FiniteType/EquivariantOrderChains.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EquivariantOrderChains.orderMap line 22
  2. def OAI.EquivariantOrderChains.simplexAct line 24
  3. instance OAI.EquivariantOrderChains.simplexAction line 28
  4. lemma OAI.EquivariantOrderChains.mapChain_id line 41
  5. lemma OAI.EquivariantOrderChains.mapChain_comp line 48
  6. def OAI.EquivariantOrderChains.action line 56
  7. lemma OAI.EquivariantOrderChains.action_val line 63
  8. def OAI.EquivariantOrderChains.representation line 66
  9. def OAI.EquivariantOrderChains.object line 82
  10. def OAI.EquivariantOrderChains.differential line 84
  11. def OAI.EquivariantOrderChains.augmentation line 92
  12. lemma OAI.EquivariantOrderChains.differential_squared line 99
  13. lemma OAI.EquivariantOrderChains.differential_aug line 104
  14. lemma OAI.EquivariantOrderChains.exact_aug line 110
  15. lemma OAI.EquivariantOrderChains.exact_succ line 115
  16. instance OAI.EquivariantOrderChains.(instance at line 121) line 121
  17. lemma OAI.EquivariantOrderChains.basisIso_single line 125
  18. lemma OAI.EquivariantOrderChains.basisIso_action line 133
  19. def OAI.EquivariantOrderChains.permutationRepresentation line 155
  20. def OAI.EquivariantOrderChains.permutationObject line 161
  21. def OAI.EquivariantOrderChains.permutationIso line 163
  22. def OAI.OrderBrown.permIso line 179
  23. def OAI.OrderBrown.C line 188
  24. def OAI.OrderBrown.d line 191
  25. lemma OAI.OrderBrown.w line 195
  26. instance OAI.OrderBrown.(instance at line 199) line 199
  27. theorem OAI.OrderBrown.vanishing line 201