OAI/GroupTheory/FiniteType/StandardHomology.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardHomology.coefficientMap line 14
  2. lemma OAI.StandardHomology.coefficientMap_naturality line 18
  3. lemma OAI.StandardHomology.inhomogeneousIso_naturality line 25
  4. def OAI.StandardHomology.chainsIso line 46
  5. lemma OAI.StandardHomology.chainsIso_naturality line 53
  6. def OAI.StandardHomology.homologyIso line 61
  7. lemma OAI.StandardHomology.homologyIso_naturality line 66
  8. instance OAI.groupHomology.chainsFunctor_additive line 82
  9. instance OAI.groupHomology.functor_additive line 99
  10. def OAI.LocalNilpotence.IsLocallyNilpotent line 110
  11. def OAI.LocalNilpotence.partialSum line 112
  12. lemma OAI.LocalNilpotence.partialSum_sub_map line 116
  13. lemma OAI.LocalNilpotence.iterate_fixed line 129
  14. theorem OAI.LocalNilpotence.one_sub_bijective line 135
  15. def OAI.LocalNilpotence.oneSubEquiv line 154
  16. theorem OAI.HomologyVanishingSequence.vanishing line 166
  17. lemma OAI.RegularProduct.shift_local_nilpotence line 192
  18. lemma OAI.RegularProduct.coset_parent_local_nilpotence line 209
  19. lemma OAI.RegularProduct.parent_local_nilpotence line 223
  20. lemma OAI.RegularProduct.boundary_bijective line 232
  21. theorem OAI.RegularProduct.vanishing line 242