OAI/RingTheory/Multiplicity/CechCarrierOperators.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Lech.CechNormalization.fullCarrier line 13
  2. abbrev OAI.Lech.CechNormalization.sortedCarrier line 14
  3. def OAI.Lech.CechNormalization.deltaOp line 16
  4. def OAI.Lech.CechNormalization.normalizeOp line 21
  5. def OAI.Lech.CechNormalization.contractionOp line 26
  6. def OAI.Lech.CechNormalization.sortOp line 31
  7. def OAI.Lech.CechNormalization.expansion line 43
  8. lemma OAI.Lech.CechNormalization.expansion_sorted line 46
  9. lemma OAI.Lech.CechNormalization.expansion_perm line 52
  10. lemma OAI.Lech.CechNormalization.expansion_degenerate line 58
  11. lemma OAI.Lech.CechNormalization.expansion_natural line 66
  12. lemma OAI.Lech.CechNormalization.expansion_agree line 80
  13. def OAI.Lech.CechNormalization.expandOp line 99
  14. def OAI.Lech.CechNormalization.sortedDeltaOp line 104
  15. lemma OAI.Lech.CechNormalization.sort_delta line 121
  16. lemma OAI.Lech.CechNormalization.sort_expand line 139
  17. lemma OAI.Lech.CechNormalization.expand_sort line 146
  18. lemma OAI.Lech.CechNormalization.expand_delta line 149