OAI/NumberTheory/PiExponent/Approximation/GeneratorsSectionCover.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PiExponent.GeneratorsSectionCover.epi_iso_comp line 13
2. abbrev OAI.PiExponent.GeneratorsSectionCover.schemeFree line 17
3. abbrev OAI.PiExponent.GeneratorsSectionCover.schemeInclusion line 20
4. def OAI.PiExponent.GeneratorsSectionCover.freeProjection line 23
5. theorem OAI.PiExponent.GeneratorsSectionCover.free_inclusion_projection line 27
6. theorem OAI.PiExponent.GeneratorsSectionCover.free_sum_projection_inclusion line 31
7. lemma OAI.PiExponent.GeneratorsSectionCover.hom_sum_app line 40
8. theorem OAI.PiExponent.GeneratorsSectionCover.unit_epimorphism_cover line 51
9. def OAI.PiExponent.GeneratorsSectionCover.generatorSection line 103
10. theorem OAI.PiExponent.GeneratorsSectionCover.generators_sectionOpen_cover line 106
11. theorem OAI.PiExponent.GeneratorsSectionCover.exists_fin_section_cover line 136
12. theorem OAI.PiExponent.GeneratorsSectionCover.ample_eventual_fin_section_cover line 147