Commit 2024-01-10 09:09 33ffe521
View on Github →feat: Add Basis.of_isLocalizedModule (#9210)
Let Mₛ be a R-module and let M be a submodule of Mₛ such that Mₛ is the localization at S of M where S is a submonoid of R. Assume that Mₛ is a Rₛ-module where Rₛ is a localization of R at S. Then, any R-basis of M is a Rₛ-basis of Mₛ.
This result is used to prove the results about Basis.localizationLocalization. For that, it is necessary to move some results between files and modify some imports.