Commit 2024-11-20 17:19 a5d04c83

chore(RingTheory): improve and generalize submodule localization API (#19118) In Algebra/Module/LocalizedModule/Submodule, we introduce Submodule.localized₀, which is localization of a submodule considered as a submodule over the base ring rather than the localization. This allows us to talk about the localization of a submodule without choosing a specific ring localization, just like what IsLocalizedModule allows us to do for localization of a module. As applications, Rₚ and every hypothesis depending on it are completely removed from the statement of Submodule.le_of_localization_maximal, etc. in RingTheory/LocalProperties/Submodule. We also reorder lemmas in this file to make the development more natural and golf the proofs (making use of Module.eqIdeal introduced in RingTheory/Ideal/Defs; also add some trivial lemmas. In RingTheory/LocalProperties/Projective, we fix a proof due to removed explicit argument Rₚ and remove some unnecessary lines.