Def TensorProduct.liftAddHom

Modification history

2023-11-27 14:14
Mathlib/LinearAlgebra/TensorProduct.lean
feat(LinearAlgebra/TensorProduct): add `liftAddHom` (#8584) …
Added TensorProduct.liftAddHomView on Github →