Commit 2025-02-05 15:13 6b45fb55

View on Github →

chore(LinearAlgebra/TensorProduct): upgrade TensorProduct.prodRight (#21432) ... to a linear map over an R-algebra S.

Estimated changes

Modified Mathlib/Algebra/Module/Equiv/Defs.lean

added theorem LinearEquiv.coe_addEquiv_apply

Modified Mathlib/LinearAlgebra/TensorProduct/Prod.lean

modified def TensorProduct.prodLeft

modified def TensorProduct.prodRight

modified theorem TensorProduct.prodRight_tmul