OAI/RingTheory/Multiplicity/KoszulSwap.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Lech.Koszul.scalarCone line 14
  2. abbrev OAI.Lech.Koszul.cInl line 15
  3. abbrev OAI.Lech.Koszul.cInr line 18
  4. abbrev OAI.Lech.Koszul.cFst line 20
  5. abbrev OAI.Lech.Koszul.cSnd line 23
  6. lemma OAI.Lech.Koszul.cInl_fst line 26
  7. lemma OAI.Lech.Koszul.cInl_snd line 28
  8. lemma OAI.Lech.Koszul.cInr_fst line 30
  9. lemma OAI.Lech.Koszul.cInr_snd line 32
  10. lemma OAI.Lech.Koszul.cInl_d line 35
  11. lemma OAI.Lech.Koszul.cInr_d line 45
  12. def OAI.Lech.Koszul.coneSwapX line 50
  13. lemma OAI.Lech.Koszul.inll_coneSwapX line 61
  14. lemma OAI.Lech.Koszul.inrl_coneSwapX line 65
  15. lemma OAI.Lech.Koszul.inlr_coneSwapX line 69
  16. lemma OAI.Lech.Koszul.inrr_coneSwapX line 73
  17. def OAI.Lech.Koszul.coneSwap line 78
  18. lemma OAI.Lech.Koszul.coneSwapX_involutive line 111
  19. def OAI.Lech.Koszul.coneSwapIso line 130
  20. def OAI.Lech.Koszul.tensorConeIso line 139