Commit 2024-11-26 20:08 b25c2968

View on Github →

chore(RingTheory/Localization): golfs and generalizations (#19310)

  • In RingTheory/LocalProperties/Basic: add some lemmas connecting localization of submodules and localization of ideals, and use results about the former to golf results about the latter.
  • In RingTheory/Localization/Module: golf a proof using the recently introduced IsLocalization.linearMap_compatibleSMul.
  • In Algebra/Module/Projective, Algebra/Module/LocalizedModule/IsLocalization, RingTheory/Localization/Submodule: generalize from AddCommGroup/CommRing to AddCommMonoid/CommSemiring. Also golf a lemma statement in the second file.
  • RingTheory/Localization/Algebra, RingTheory/Localization/Ideal: add two TODOs that are not done here for import reasons.

Estimated changes

modified theorem IsLocalization.mem_span_iff