OAI/RingTheory/Multiplicity/ReesCoordinate.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Lech.ProjectiveRoot.ratioline 13 - lemma
OAI.Lech.ProjectiveRoot.scalarMap_ratioline 15 - lemma
OAI.Lech.ProjectiveRoot.ratio_mkline 19 - lemma
OAI.Lech.ReesRoot.generator_relationline 45 - lemma
OAI.Lech.ReesRoot.ratio_relationline 59