OAI/NumberTheory/PiExponent/Approximation/TwistSectionClearing.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PiExponent.TwistSectionClearing.iso_section_restrict_zero line 14
2. lemma OAI.PiExponent.TwistSectionClearing.frame_local_input_zero line 24
3. lemma OAI.PiExponent.TwistSectionClearing.section_zero_of_imageTop line 44
4. lemma OAI.PiExponent.TwistSectionClearing.iso_section_restrict_zero_on line 49
5. lemma OAI.PiExponent.TwistSectionClearing.frame_local_input_zero_on line 59
6. theorem OAI.PiExponent.TwistSectionClearing.frame_twistForward_zero_on line 84
7. lemma OAI.PiExponent.TwistSectionClearing.hom_section_restriction line 108
8. theorem OAI.PiExponent.TwistSectionClearing.frame_twistForward_ambient_zero line 115
9. theorem OAI.PiExponent.TwistSectionClearing.twistForward_section_zero line 142
10. theorem OAI.PiExponent.TwistSectionClearing.twistSection_zero line 171