Commit 2025-11-10 09:40 3f0f0512

View on Github →

feat(TensorProduct): lTensor as an AlgHom and other lemmas (#28973) From Toric

Estimated changes

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

added theorem Algebra.TensorProduct.algebraMap_def

added theorem Algebra.TensorProduct.algebraMap_eq_includeRight

Modified Mathlib/RingTheory/TensorProduct/Maps.lean

added theorem Algebra.TensorProduct.toLinearMap_map