OAI/RingTheory/Multiplicity/TorsionThickening.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Lech.TwistedLocalization.piece_torsionline 17 - def
OAI.Lech.TwistedLocalization.gradedKernelEquivline 34 - lemma
OAI.Lech.TwistedLocalization.kernel_zeroClassline 47 - lemma
OAI.Lech.SourceGraded.twist_kernel_zeroClassline 82 - lemma
OAI.Lech.SourceGraded.exceptionalCech_homology_zeroClassline 91 - lemma
OAI.Lech.SourceGraded.finiteThickening_homology_zeroClassline 102 - lemma
OAI.Lech.SourceGraded.finiteThickening_totalTensor_zeroClassline 125 - lemma
OAI.Lech.SourceGraded.thickeningComparison_isoModSerre_torsionline 136