Commit 2024-12-20 22:32 31e1a94c

View on Github →

feat(RingTheory/Flat): generalize flat_of_isLocalized_span (#19788) Generalize Module.Flat.flat_of_isLocalized_span to take s : Set S for any R-algebra S.

Estimated changes

Modified Mathlib/Algebra/Equiv/TransferInstance.lean

added theorem LinearEquiv.isScalarTower

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

added theorem TensorProduct.AlgebraTensorModule.coe_rTensor

added def TensorProduct.AlgebraTensorModule.rTensor

added theorem TensorProduct.AlgebraTensorModule.rTensor_comp

added theorem TensorProduct.AlgebraTensorModule.rTensor_id

added theorem TensorProduct.AlgebraTensorModule.rTensor_mul

added theorem TensorProduct.AlgebraTensorModule.rTensor_one

added theorem TensorProduct.AlgebraTensorModule.rTensor_tmul

added theorem TensorProduct.AlgebraTensorModule.restrictScalars_rTensor

Modified Mathlib/RingTheory/Flat/Basic.lean

Modified Mathlib/RingTheory/Flat/Localization.lean

deleted theorem Module.flat_of_isLocalized_maixmal

added theorem Module.flat_of_isLocalized_maximal

Modified Mathlib/RingTheory/IsTensorProduct.lean

added theorem IsBaseChange.of_equiv

added theorem IsTensorProduct.of_equiv

added theorem isBaseChange_tensorProduct_map

Modified Mathlib/RingTheory/Localization/BaseChange.lean

added theorem IsLocalizedModule.map_lTensor

Modified Mathlib/RingTheory/Localization/Module.lean

added theorem LocalizedModule.restrictScalars_map_eq