OAI/NumberTheory/PiExponent/LocalAlgebra/IdealSectionRestriction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.IdealSectionRestriction.sectionsEquiv line 12
  2. theorem OAI.PiExponent.IdealSectionRestriction.sectionsEquiv_inclusion line 18
  3. theorem OAI.PiExponent.IdealSectionRestriction.inclusion_injective line 25
  4. def OAI.PiExponent.IdealSectionRestriction.pullback line 31
  5. theorem OAI.PiExponent.IdealSectionRestriction.pullback_inclusion line 37
  6. theorem OAI.PiExponent.IdealSectionRestriction.pullback_eq_sectionsEquiv line 52
  7. def OAI.PiExponent.IdealSectionRestriction.idealCongr line 62
  8. theorem OAI.PiExponent.IdealSectionRestriction.idealCongr_inclusion line 67
  9. theorem OAI.PiExponent.IdealSectionRestriction.pullback_comp line 73
  10. theorem OAI.PiExponent.IdealSectionRestriction.pullback_self line 91
  11. theorem OAI.PiExponent.IdealSectionRestriction.pullback_bijective_iff_comap line 99