OAI/GroupTheory/SimpleAmenable/Simplicial/FinitePowerLow.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BarFinitePower.LowFinite line 11
  2. lemma OAI.BarFinitePower.LowFinite.of_iso line 16
  3. lemma OAI.BarFinitePower.LowFinite.one line 23
  4. lemma OAI.BarFinitePower.LowFinite.projection_isIso line 32
  5. lemma OAI.BarFinitePower.LowFinite.tensor line 41
  6. lemma OAI.BarFinitePower.LowFinite.fin line 55
  7. lemma OAI.BarFinitePower.LowFinite.power line 59
  8. def OAI.BarFinitePower.coordinates line 70
  9. lemma OAI.BarFinitePower.coordinates_evaluate line 72
  10. lemma OAI.BarFinitePower.modulePi_hom_ext line 74
  11. def OAI.BarFinitePower.vectorSplit line 79
  12. def OAI.BarFinitePower.coordinateSplit line 86
  13. lemma OAI.BarFinitePower.coordinateSplit_fst line 88
  14. lemma OAI.BarFinitePower.coordinateSplit_snd_proj line 92
  15. lemma OAI.BarFinitePower.coordinates_fin_succ line 101
  16. lemma OAI.BarFinitePower.coordinates_fin_isIso line 121
  17. def OAI.BarFinitePower.coefficientReindex line 138
  18. lemma OAI.BarFinitePower.coordinates_reindex line 148
  19. lemma OAI.BarFinitePower.coordinates_isIso line 158