OAI/RingTheory/Multiplicity/ReesRootGLayerCohomology.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.Lech.ReesRoot.exceptionalZline 19 - lemma
OAI.Lech.ReesRoot.exceptionalZ_negativeline 22 - lemma
OAI.Lech.ReesRoot.exceptionalZ_torsionline 30 - lemma
OAI.Lech.ReesRoot.exceptionalZ_finiteline 39 - lemma
OAI.Lech.ReesRoot.exceptionalZ_zeroline 48 - def
OAI.Lech.ReesRoot.layerAtRowHomologyBasisIsoline 66 - lemma
OAI.Lech.ReesRoot.layerAtRow_torsionline 74 - lemma
OAI.Lech.ReesRoot.layerAtRow_lengthline 80 - lemma
OAI.Lech.ReesRoot.layerAtRow_finiteline 89 - lemma
OAI.Lech.ReesRoot.layerAtRow_zeroline 95