OAI/GroupTheory/SimpleAmenable/Homology/RegularCoefficientDouble.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RegularCoefficient.iso_transport_cancel line 13
  2. lemma OAI.RegularCoefficient.inverse_square_of_identity line 19
  3. def OAI.RegularCoefficient.coeffComplex line 27
  4. def OAI.RegularCoefficient.evalHomology line 29
  5. lemma OAI.RegularCoefficient.evalHomology_natural line 32
  6. def OAI.RegularCoefficient.homologyZeroIso line 42
  7. lemma OAI.RegularCoefficient.positive_isZero line 53
  8. def OAI.RegularCoefficient.double line 57
  9. def OAI.RegularCoefficient.rowZeroIso line 58
  10. lemma OAI.RegularCoefficient.row_positive_isZero line 61
  11. lemma OAI.RegularCoefficient.total_finite line 65
  12. abbrev OAI.RegularCoordinates.B line 85
  13. lemma OAI.RegularCoordinates.opposite_eqToHom_val line 86
  14. lemma OAI.RegularCoordinates.single_eqToHom_val line 87
  15. def OAI.RegularCoordinates.lift line 88
  16. lemma OAI.RegularCoordinates.lift_right line 102
  17. lemma OAI.RegularCoordinates.lift_project line 106
  18. lemma OAI.RegularCoordinates.lift_recover line 113
  19. def OAI.RegularCoordinates.coordinates line 125
  20. lemma OAI.RegularCoordinates.shift_right line 130
  21. lemma OAI.RegularCoordinates.shift_project line 132
  22. lemma OAI.RegularCoordinates.shift_lift line 140