OAI/RingTheory/Multiplicity/CechCartierRange.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Lech.TensorIdeal.piMap_rangeline 14 - lemma
OAI.Lech.ReesRoot.cechInclusionIterApp_rangeline 51 - lemma
OAI.Lech.ReesRoot.cechInclusionIter_rangeline 61 - lemma
OAI.Lech.ReesRoot.cechInclusionIter_injectiveline 70 - instance
OAI.Lech.ReesRoot.cechInclusionIter_monoline 76