Def PiTensorProduct.mapMonoidHom

Modification history

2024-03-08 09:46

Mathlib/LinearAlgebra/PiTensorProduct.lean

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

Added PiTensorProduct.mapMonoidHom View on Github →