OAI/NumberTheory/PiExponent/Approximation/TwistSectionScalars.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PiExponentSeshadri.Geometry.moduleSectionMultiplyRight_pure line 12
2. lemma OAI.PiExponentSeshadri.Geometry.moduleTensorFrame_pure line 31
3. lemma OAI.PiExponentSeshadri.Geometry.moduleSectionMultiplyRight_frame line 41
4. lemma OAI.PiExponentSeshadri.Geometry.moduleSectionMultiplyRight_restrict_frame line 49
5. lemma OAI.PiExponentSeshadri.Geometry.moduleTwistForward_frame line 78
6. lemma OAI.PiExponentSeshadri.Geometry.moduleTwistSection_frame line 98