theorem LinearMap.localized'_range_eq_range_localizedMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Submonoid R) [IsLocalization p S] {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[R] N) [IsLocalizedModule p f] {P : Type u_5} {Q : Type u_6} [AddCommGroup P] [Module R P] [AddCommGroup Q] [Module R Q] [Module S Q] [IsScalarTower R S Q] (f' : P →ₗ[R] Q) [IsLocalizedModule p f'] (g : M →ₗ[R] P) : Submodule.localized' S p f' (LinearMap.range g) = LinearMap.range (LinearMap.extendScalarsOfIsLocalization p S ((IsLocalizedModule.map p f f') g))