OAI/NumberTheory/PiExponent/Approximation/TwistGlobalExtension.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PiExponent.TwistGlobalExtension.section_open_image line 15
2. theorem OAI.PiExponent.TwistGlobalExtension.local_twist_extension_ambient line 25
3. theorem OAI.PiExponent.TwistGlobalExtension.finite_local_twist_extensions line 60
4. lemma OAI.PiExponent.TwistGlobalExtension.mapSection_twistSection_add line 79
5. theorem OAI.PiExponent.TwistGlobalExtension.finite_cover_twist_gluing line 86
6. theorem OAI.PiExponent.TwistGlobalExtension.exists_global_twist_extension line 126
7. theorem OAI.PiExponent.TwistGlobalExtension.global_twist_extension line 149
8. theorem OAI.PiExponent.TwistGlobalExtension.global_twist_extension_native line 163