OAI/RingTheory/Multiplicity/MinimalComplex.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Lech.exists_minimal_complex line 14
2. theorem OAI.Lech.IsShortComplex.exists_minimal line 33
3. lemma OAI.Lech.shortEuler_eq_of_homotopyEquiv line 43
4. lemma OAI.Lech.duttaSequence_eq_of_homotopyEquiv line 50
5. lemma OAI.Lech.duttaMultiplicity_eq_of_homotopyEquiv line 58