OAI/GroupTheory/SimpleAmenable/Homology/BooleanStepCoefficients.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SimpleAmenable.PolygonObject.BooleanPartition.arrangement_color line 16
  2. lemma OAI.SimpleAmenable.PolygonObject.BooleanPartition.arrangement_values line 21
  3. lemma OAI.SimpleAmenable.PolygonObject.BooleanPartition.exists_arrangement_partition line 26
  4. def OAI.SimpleAmenable.PolygonObject.booleanStepSubmodule line 37
  5. abbrev OAI.SimpleAmenable.PolygonObject.BooleanStep line 48
  6. def OAI.SimpleAmenable.PolygonObject.BooleanStep.inflate line 51
  7. def OAI.SimpleAmenable.PolygonObject.BooleanStep.evaluate line 55
  8. lemma OAI.SimpleAmenable.PolygonObject.BooleanStep.inflate_apply line 60
  9. lemma OAI.SimpleAmenable.PolygonObject.BooleanStep.evaluate_apply line 63
  10. lemma OAI.SimpleAmenable.PolygonObject.BooleanStep.evaluate_inflate line 66
  11. lemma OAI.SimpleAmenable.PolygonObject.BooleanStep.inflate_injective line 70
  12. def OAI.SimpleAmenable.PolygonObject.BooleanStep.refinement line 75
  13. lemma OAI.SimpleAmenable.PolygonObject.BooleanStep.inflate_refinement line 78
  14. lemma OAI.SimpleAmenable.PolygonObject.BooleanStep.exists_common line 84
  15. def OAI.SimpleAmenable.PolygonObject.BooleanStep.multiply line 100
  16. def OAI.SimpleAmenable.PolygonObject.BooleanStep.tensorMap line 112
  17. lemma OAI.SimpleAmenable.PolygonObject.BooleanStep.tensorMap_tmul line 114
  18. def OAI.SimpleAmenable.PolygonObject.BooleanStep.finiteTensorEquiv line 116
  19. lemma OAI.SimpleAmenable.PolygonObject.BooleanStep.finiteTensorEquiv_tmul line 119
  20. def OAI.SimpleAmenable.PolygonObject.BooleanStep.tensorInflate line 123
  21. lemma OAI.SimpleAmenable.PolygonObject.BooleanStep.tensorMap_inflate line 126
  22. lemma OAI.SimpleAmenable.PolygonObject.BooleanStep.tensorInflate_refinement line 132
  23. lemma OAI.SimpleAmenable.PolygonObject.BooleanStep.exists_tensor_stage line 137
  24. lemma OAI.SimpleAmenable.PolygonObject.BooleanStep.tensorMap_injective line 156
  25. lemma OAI.SimpleAmenable.PolygonObject.BooleanStep.tensorMap_surjective line 168
  26. def OAI.SimpleAmenable.PolygonObject.BooleanStep.tensorEquiv line 176