OAI/NumberTheory/PiExponent/Approximation/GlobalSectionClearing.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.GlobalSectionClearing.restrictScalar line 11
  2. lemma OAI.PiExponent.GlobalSectionClearing.restrictScalar_naturality line 14
  3. def OAI.PiExponent.GlobalSectionClearing.OpenSections line 20
  4. instance OAI.PiExponent.GlobalSectionClearing.(instance at line 21) line 21
  5. instance OAI.PiExponent.GlobalSectionClearing.(instance at line 23) line 23
  6. def OAI.PiExponent.GlobalSectionClearing.openRestriction line 26
  7. theorem OAI.PiExponent.GlobalSectionClearing.quasicoherent_pushforward_iso line 38
  8. abbrev OAI.PiExponent.GlobalSectionClearing.affineToSpecModule line 50
  9. instance OAI.PiExponent.GlobalSectionClearing.affineToSpecModule_quasicoherent line 53
  10. theorem OAI.PiExponent.GlobalSectionClearing.affine_sections_localize line 57
  11. def OAI.PiExponent.GlobalSectionClearing.affineSpecSections line 64
  12. def OAI.PiExponent.GlobalSectionClearing.openSectionsCongr line 90
  13. lemma OAI.PiExponent.GlobalSectionClearing.openSectionsCongr_restriction line 95
  14. theorem OAI.PiExponent.GlobalSectionClearing.affine_openRestriction_localize line 101
  15. theorem OAI.PiExponent.GlobalSectionClearing.affine_basicOpen_denominators line 120
  16. def OAI.PiExponent.GlobalSectionClearing.openTopSections line 129
  17. lemma OAI.PiExponent.GlobalSectionClearing.restrictScalar_appIso line 147
  18. def OAI.PiExponent.GlobalSectionClearing.restrictedOpenSections line 159
  19. lemma OAI.PiExponent.GlobalSectionClearing.restrictedOpenSections_naturality line 177
  20. theorem OAI.PiExponent.GlobalSectionClearing.affine_basicOpen_zero line 182
  21. lemma OAI.PiExponent.GlobalSectionClearing.openRestriction_comp_apply line 194
  22. lemma OAI.PiExponent.GlobalSectionClearing.openRestriction_zero_congr line 201
  23. lemma OAI.PiExponent.GlobalSectionClearing.affine_immersion_zero_on line 207
  24. theorem OAI.PiExponent.GlobalSectionClearing.compact_open_section_zero line 237
  25. theorem OAI.PiExponent.GlobalSectionClearing.global_section_zero line 270
  26. lemma OAI.PiExponent.GlobalSectionClearing.openSectionsCongr_naturality line 277
  27. lemma OAI.PiExponent.GlobalSectionClearing.principal_open_image line 285
  28. def OAI.PiExponent.GlobalSectionClearing.affineOpenPrincipalEquiv line 290
  29. def OAI.PiExponent.GlobalSectionClearing.affineOpenTopEquiv line 297
  30. lemma OAI.PiExponent.GlobalSectionClearing.affineOpenPrincipalEquiv_restrict line 302
  31. theorem OAI.PiExponent.GlobalSectionClearing.affine_open_section_extends line 312
  32. def OAI.PiExponent.GlobalSectionClearing.overlapDifference line 331
  33. lemma OAI.PiExponent.GlobalSectionClearing.overlapDifference_restrict_zero line 335
  34. lemma OAI.PiExponent.GlobalSectionClearing.overlapDifference_smul_zero_iff line 354
  35. theorem OAI.PiExponent.GlobalSectionClearing.clear_finite_overlap_discrepancies line 361
  36. lemma OAI.PiExponent.GlobalSectionClearing.restriction_of_glued_power line 380
  37. theorem OAI.PiExponent.GlobalSectionClearing.finite_cover_power_gluing line 398
  38. theorem OAI.PiExponent.GlobalSectionClearing.finite_affine_local_extensions line 415
  39. theorem OAI.PiExponent.GlobalSectionClearing.global_section_extends line 429
  40. theorem OAI.PiExponent.GlobalSectionClearing.global_section_extends_native line 450
  41. theorem OAI.PiExponent.GlobalSectionClearing.global_section_zero_native line 467