Commit 2024-12-09 09:39 a2702bb7
View on Github →feat(TensorProduct): change of base ring in tensor product of algebras (#19670)
A follow up to #18744, adding more contents about tensor product of algebras.
In LinearAlgebra/TensorProduct/Basic.lean: change the argument order of mapOfCompatibleSMul from R M N A to the more natural R A M N; add lidOfCompatibleSMul.
In RingTheory/TensorProduct/Basic.lean: add a CompatibleSMul section for algebras completely analogous to the CompatibleSMul section in LinearAlgebra/TensorProduct/Basic.lean added in #18744.
In RingTheory/Localization/BaseChange.lean: promote various examples to defs, and generalize tensorSelfEquiv to algebraLid.