OAI/GroupTheory/FiniteType/CosetInduction.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CosetInduction.cosetRep line 13
  2. lemma OAI.CosetInduction.subgroup_fixes_base line 15
  3. def OAI.CosetInduction.baseHom line 20
  4. def OAI.CosetInduction.indToCosets line 29
  5. lemma OAI.CosetInduction.indToCosets_mk line 32
  6. lemma OAI.CosetInduction.ind_mk_left line 41
  7. def OAI.CosetInduction.cosetSection line 49
  8. lemma OAI.CosetInduction.cosetSection_mk line 61
  9. def OAI.CosetInduction.cosetsToInd line 65
  10. lemma OAI.CosetInduction.cosetsToInd_single line 68
  11. lemma OAI.CosetInduction.cosetsToInd_indToCosets line 72
  12. lemma OAI.CosetInduction.indToCosets_cosetsToInd line 84
  13. def OAI.CosetInduction.indCosetIso line 96
  14. def OAI.StandardShapiro.cosetCoefficientIso line 117
  15. def OAI.StandardShapiro.cosetEquiv line 123
  16. lemma OAI.StandardShapiro.cosetEquiv_hom_f_mk_tmul line 128
  17. def OAI.ExactTargetHomotopy.stepZero line 154
  18. lemma OAI.ExactTargetHomotopy.stepZero_comp line 157
  19. def OAI.ExactTargetHomotopy.stepOne line 160
  20. lemma OAI.ExactTargetHomotopy.stepOne_comp line 166
  21. def OAI.ExactTargetHomotopy.stepSucc line 171
  22. lemma OAI.ExactTargetHomotopy.stepSucc_comp line 179
  23. def OAI.ExactTargetHomotopy.nullHomotopy line 185
  24. def OAI.ExactTargetHomotopy.comparison line 191
  25. lemma OAI.StandardVertex.augmentation_eq line 204
  26. def OAI.StandardVertex.homotopy line 220