OAI/GroupTheory/SimpleAmenable/Homology/VerticalStringResolution.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.VerticalString.allowed line 19
  2. abbrev OAI.SimpleAmenable.VerticalString.Object line 22
  3. def OAI.SimpleAmenable.VerticalString.evaluation line 24
  4. def OAI.SimpleAmenable.VerticalString.constant line 30
  5. def OAI.SimpleAmenable.VerticalString.comparison line 37
  6. def OAI.SimpleAmenable.VerticalString.evaluationEquivalence line 74
  7. def OAI.SimpleAmenable.VerticalString.polygonEvaluationEquivalence line 86
  8. def OAI.SimpleAmenable.IntegralTransgression.Kernel line 99
  9. instance OAI.SimpleAmenable.IntegralTransgression.kernelCommGroup line 101
  10. def OAI.SimpleAmenable.IntegralTransgression.inclusion line 107
  11. def OAI.SimpleAmenable.IntegralTransgression.sectionMap line 112
  12. theorem OAI.SimpleAmenable.IntegralTransgression.section_one line 114
  13. theorem OAI.SimpleAmenable.IntegralTransgression.section_projection line 115
  14. def OAI.SimpleAmenable.IntegralTransgression.factor line 120
  15. def OAI.SimpleAmenable.IntegralTransgression.remainder line 125
  16. theorem OAI.SimpleAmenable.IntegralTransgression.factor_one_left line 130
  17. theorem OAI.SimpleAmenable.IntegralTransgression.factor_one_right line 132
  18. theorem OAI.SimpleAmenable.IntegralTransgression.remainder_one line 134
  19. theorem OAI.SimpleAmenable.IntegralTransgression.remainder_inclusion line 136
  20. theorem OAI.SimpleAmenable.IntegralTransgression.factor_cocycle line 143
  21. theorem OAI.SimpleAmenable.IntegralTransgression.remainder_mul line 162