OAI/NumberTheory/PiExponent/Approximation/FrameSubopens.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.PiExponentSeshadri.Frames.restrictOpenFrameline 10 - lemma
OAI.PiExponentSeshadri.Frames.restrictOpenFrame_coefficient_globalline 16 - lemma
OAI.PiExponentSeshadri.Frames.frameChange_restrictOpenFrameline 29