OAI/GroupTheory/SimpleAmenable/Homology/QuotientRegular.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.QuotientRegular.regular line 17
  2. def OAI.QuotientRegular.point line 20
  3. def OAI.QuotientRegular.kernelEquivStabilizer line 29
  4. def OAI.QuotientRegular.permutationIso line 38
  5. lemma OAI.QuotientRegular.isIso_point line 51
  6. def OAI.QuotientRegular.right line 82
  7. lemma OAI.QuotientRegular.right_single line 91
  8. def OAI.QuotientRegular.conjugate line 95
  9. lemma OAI.QuotientRegular.right_homology_identity line 98
  10. lemma OAI.QuotientRegular.H1_isZero line 125
  11. lemma OAI.QuotientRegular.H2_finite_of_regular line 131
  12. def OAI.FiniteFreeRep.incl line 150
  13. def OAI.FiniteFreeRep.proj line 157
  14. lemma OAI.FiniteFreeRep.sum_proj_incl line 166
  15. lemma OAI.FiniteFreeRep.functor_isZero line 174
  16. lemma OAI.FiniteFreeRep.functor_finite line 182
  17. instance OAI.FiniteFreeRep.finite_free line 197
  18. lemma OAI.FiniteFreeRep.exists_cover line 201
  19. lemma OAI.FiniteFreeRep.finite_kernel line 218