OAI/RingTheory/Multiplicity/ComplexTensorComparison.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Lech.tensorModuleFunctor line 13
2. instance OAI.Lech.tensorModuleFunctor_additive line 22
3. lemma OAI.Lech.tensorModuleFunctor_smul line 29
4. def OAI.Lech.tensorModuleUnitIso line 39
5. lemma OAI.Lech.tensorModule_homology_length_free line 49
6. theorem OAI.Lech.exists_tensor_homology_bound line 62