Def PiTensorProduct.mapIncl

Modification history

2024-03-08 09:46

Mathlib/LinearAlgebra/PiTensorProduct.lean

feat(LinearAlgebra/PiTensorProduct): some more functoriality properties of `PiTensorProduct` (#11152) …

Added PiTensorProduct.mapIncl View on Github →