OAI/RingTheory/Multiplicity/CechCartierZRange.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.Lech.TensorIdeal.range_of_squareline 14 - lemma
OAI.Lech.TensorIdeal.injective_of_squareline 25 - lemma
OAI.Lech.ReesRoot.cechInclusionZ_squareline 43 - lemma
OAI.Lech.ReesRoot.cechInclusionZ_rangeline 59 - lemma
OAI.Lech.ReesRoot.cechInclusionZ_injectiveline 72