Commit 2023-07-29 18:51 d8f68396

View on Github →

feat: add IsLocalizedModule.isBaseChange (#5766) Port of leanprover-community/mathlib#17973 Follow up work:

add IsPushout when M is a CommRing.

Estimated changes

Modified Mathlib/Algebra/Module/LocalizedModule.lean

added theorem IsLocalizedModule.isBaseChange

Modified Mathlib/LinearAlgebra/TensorProduct.lean

added theorem TensorProduct.exists_eq_tmul_of_forall

Modified Mathlib/RingTheory/Localization/Basic.lean

added theorem IsLocalization.smul_mk'

added theorem IsLocalization.smul_mk'_one

added theorem IsLocalization.smul_mk'_self

Modified Mathlib/RingTheory/Localization/Module.lean

added def LinearMap.extendScalarsOfIsLocalization

added theorem LinearMap.extendScalarsOfIsLocalization_apply

added theorem LinearMap.restrictScalars_extendScalarsOfIsLocalization