OAI/GroupTheory/FiniteType/SemilinearCoinvariants.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SemilinearCoinvariants.tensorNatTrans line 14
  2. lemma OAI.SemilinearCoinvariants.tensorNatTrans_mk_tmul line 20
  3. def OAI.SemilinearCoinvariants.chainMap line 29
  4. lemma OAI.SemilinearCoinvariants.chainMap_f_mk_tmul line 35
  5. def OAI.SemilinearCoinvariants.chainMapHomotopy line 47
  6. lemma OAI.CosetEndpoint.inv_mul_subtype line 61
  7. def OAI.CosetEndpoint.shiftCoeff line 65
  8. def OAI.CosetEndpoint.shiftChain line 72
  9. def OAI.CosetEndpoint.baseShiftCoeff line 78
  10. lemma OAI.CosetEndpoint.baseShiftCoeff_apply line 82
  11. lemma OAI.CosetEndpoint.leftVertex_equivariant line 87
  12. def OAI.CosetEndpoint.leftVertexMap line 93
  13. def OAI.CosetEndpoint.rightVertexMap line 96
  14. def OAI.CosetEndpoint.leftChain line 99
  15. def OAI.CosetEndpoint.rightChain line 103
  16. def OAI.CosetEndpoint.endpointHomotopy line 107
  17. def OAI.StandardTensor.coefficientMap line 120
  18. lemma OAI.StandardTensor.coefficientMap_f_mk_tmul line 125
  19. lemma OAI.StandardTensor.chain_ext line 130
  20. lemma OAI.StandardTensor.semilinear_single line 152
  21. lemma OAI.StandardTensor.shapiro_single line 164
  22. lemma OAI.CosetEndpoint.shapiro_parent_eq_left line 185
  23. lemma OAI.CosetEndpoint.shift_shapiro_eq_right line 233
  24. def OAI.CosetEndpoint.shapiroParentHomotopy line 247