OAI/NumberTheory/PiExponent/LocalAlgebra/FiniteSupportLocalIso.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PiExponentSeshadri.Geometry.openSectionModuleline 13 - def
OAI.PiExponentSeshadri.Geometry.openSectionRestrictionline 17 - def
OAI.PiExponentSeshadri.Geometry.disjointSupportCoverEquivline 23 - def
OAI.PiExponentSeshadri.Geometry.openSectionIsoline 46 - def
OAI.PiExponentSeshadri.Geometry.finiteSupportLocallyIsoGloballine 73