Equivalence between IsLocalizedModule and IsLocalization

theorem isLocalizedModule_iff_isLocalization {R : Type u_1} [CommSemiring R] {S : Submonoid R} {A : Type u_2} {Aₛ : Type u_3} [CommSemiring A] [Algebra R A] [CommSemiring Aₛ] [Algebra A Aₛ] [Algebra R Aₛ] [IsScalarTower R A Aₛ] : IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap ↔ IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ

instance instIsLocalizedModuleToLinearMapToAlgHomOfIsLocalizationAlgebraMapSubmonoid {R : Type u_1} [CommSemiring R] (S : Submonoid R) {A : Type u_2} {Aₛ : Type u_3} [CommSemiring A] [Algebra R A] [CommSemiring Aₛ] [Algebra A Aₛ] [Algebra R Aₛ] [IsScalarTower R A Aₛ] [h : IsLocalization (Algebra.algebraMapSubmonoid A S) Aₛ] : IsLocalizedModule S (IsScalarTower.toAlgHom R A Aₛ).toLinearMap

theorem isLocalizedModule_iff_isLocalization' {R : Type u_1} [CommSemiring R] (S : Submonoid R) (R' : Type u_2) [CommSemiring R'] [Algebra R R'] : IsLocalizedModule S (Algebra.linearMap R R') ↔ IsLocalization S R'

instance instIsLocalizedModuleLinearMapOfIsLocalization {R : Type u_1} [CommSemiring R] (S : Submonoid R) {A : Type u_2} [CommSemiring A] [Algebra R A] [IsLocalization S A] : IsLocalizedModule S (Algebra.linearMap R A)