OAI/RingTheory/Multiplicity/RootCechCoefficients.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Lech.ProjectiveRoot.coefficientCech line 15
2. def OAI.Lech.ProjectiveRoot.coefficientHomologyIso line 17
3. lemma OAI.Lech.ProjectiveRoot.coefficient_pure line 25
4. def OAI.Lech.ProjectiveRoot.coefficientHomologySelfIso line 30
5. abbrev OAI.Lech.ProjectiveRoot.tensorCech line 37
6. def OAI.Lech.ProjectiveRoot.integerHomologyBasis line 39
7. def OAI.Lech.ProjectiveRoot.tensorHomologyEquiv line 47
8. lemma OAI.Lech.ProjectiveRoot.tensor_pure line 54