OAI/RingTheory/Multiplicity/CechNormalizationRows.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.CechNormalization.sortedRestriction line 13
  2. def OAI.Lech.CechNormalization.altify line 18
  3. def OAI.Lech.CechNormalization.normalize line 21
  4. lemma OAI.Lech.CechNormalization.normalize_sorted line 24
  5. lemma OAI.Lech.CechNormalization.altify_delta line 33
  6. lemma OAI.Lech.CechNormalization.normalize_delta line 55
  7. lemma OAI.Lech.CechNormalization.normalize_zero line 61
  8. lemma OAI.Lech.CechNormalization.normalize_perm line 67
  9. lemma OAI.Lech.CechNormalization.normalize_degenerate line 72
  10. def OAI.Lech.CechNormalization.AgreeOn line 80
  11. lemma OAI.Lech.CechNormalization.normalize_agree line 83
  12. lemma OAI.Lech.CechNormalization.normalize_natural line 99
  13. lemma OAI.Lech.CechNormalization.delta_natural line 113
  14. lemma OAI.Lech.CechNormalization.delta_agree line 119
  15. lemma OAI.Lech.CechNormalization.extra_agree line 130
  16. def OAI.Lech.CechNormalization.contraction line 139
  17. lemma OAI.Lech.CechNormalization.contraction_succ line 147
  18. lemma OAI.Lech.CechNormalization.contraction_identity_step line 152
  19. lemma OAI.Lech.CechNormalization.contraction_identity line 173
  20. lemma OAI.Lech.CechNormalization.contraction_natural line 188
  21. lemma OAI.Lech.CechNormalization.contraction_agree line 201