OAI/NumberTheory/PiExponent/Approximation/PowerSectionExtension.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PiExponentSeshadri.Frames.coefficient_scalarEnd line 13
2. lemma OAI.PiExponentSeshadri.Geometry.affine_function_denom line 28
3. theorem OAI.PiExponentSeshadri.Geometry.local_affine_power_extension line 38
4. theorem OAI.PiExponentSeshadri.Geometry.LineBundle.glue_dense_subopens line 78
5. theorem OAI.PiExponentSeshadri.Geometry.LineBundle.finite_cover_power_extension line 121
6. def OAI.PiExponentSeshadri.InvertibleLocal.frameOfLE line 199
7. lemma OAI.PiExponentSeshadri.InvertibleLocal.affine_frame line 208
8. theorem OAI.PiExponentSeshadri.Geometry.LineBundle.power_extension line 223