Commit 2026-05-25 15:44 fbeb4b7b

View on Github →

chore(RingTheory/TensorProduct/Basic): some API for includeLeft and includeRight (#39694)

Estimated changes

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

added theorem TensorProduct.AlgebraTensorModule.mk_eq

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

added theorem Algebra.TensorProduct.toLinearMap_includeLeft

added theorem Algebra.TensorProduct.toLinearMap_includeRight

Modified Mathlib/RingTheory/TensorProduct/IncludeLeftSubRight.lean