OAI/RingTheory/Multiplicity/TensorEuler.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.ordinaryLength_real line 15
2. lemma OAI.Lech.ordinaryLength_finite line 25
3. lemma OAI.Lech.shortEuler_additive line 32
4. lemma OAI.Lech.tensorModule_shortExact line 82
5. lemma OAI.Lech.tensorModule_homology_finite line 94
6. lemma OAI.Lech.tensorModule_homology_bounded line 119
7. lemma OAI.Lech.shortEuler_eq_of_iso line 128
8. lemma OAI.Lech.tensorEuler_equiv line 136