Theorem Algebra.TensorProduct.toLinearMap_includeRight

Modification history

2026-05-25 15:44

Mathlib/RingTheory/TensorProduct/Basic.lean

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

Added Algebra.TensorProduct.toLinearMap_includeRight View on Github →