OAI/Combinatorics/Chromatic/Walls/CompletedCutAction.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.RationalFiber.shearRatio_inv_val_add line 13
  2. def OAI.ElementaryPositivity.RationalFiber.shearActionInvHom line 17
  3. lemma OAI.ElementaryPositivity.RationalFiber.shearAction_cancel line 20
  4. lemma OAI.ElementaryPositivity.RationalFiber.shearActionInv_cancel line 26
  5. def OAI.ElementaryPositivity.RationalFiber.shearAction line 32
  6. def OAI.ElementaryPositivity.RationalFiber.completedShearAction line 35
  7. def OAI.ElementaryPositivity.RationalFiber.completedOppositeInverseAction line 41
  8. lemma OAI.ElementaryPositivity.RationalFiber.completed_cut_identity line 45
  9. lemma OAI.ElementaryPositivity.RationalFiber.completedOppositeInverseAction_eq line 56
  10. lemma OAI.ElementaryPositivity.RationalFiber.completedShearAction_embed line 62
  11. def OAI.ElementaryPositivity.RationalFiber.mutationSideAction line 84
  12. lemma OAI.ElementaryPositivity.RationalFiber.mutationSideAction_cut line 88
  13. lemma OAI.ElementaryPositivity.RationalFiber.mutationSideAction_cut_reverse line 94
  14. lemma OAI.ElementaryPositivity.RationalFiber.mutationSideAction_inner line 100
  15. def OAI.ElementaryPositivity.RationalFiber.covectorSideAction line 122
  16. def OAI.ElementaryPositivity.RationalFiber.pushedRationalTransport line 131
  17. lemma OAI.ElementaryPositivity.RationalFiber.pushedRationalTransport_apply line 137
  18. lemma OAI.ElementaryPositivity.RationalFiber.pushedRationalTransport_self line 146
  19. lemma OAI.ElementaryPositivity.RationalFiber.pushedRationalTransport_trans line 153