Theorem PiTensorProduct.map_tprod

Modification history

2024-03-08 09:46

Mathlib/LinearAlgebra/PiTensorProduct.lean

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

Modified PiTensorProduct.map_tprod View on Github →

2024-03-02 20:50

Mathlib/LinearAlgebra/PiTensorProduct.lean

feat(LinearAlgebra/PiTensorProduct): arbitrary tensor product of algebras (#9395) …

Added PiTensorProduct.map_tprod View on Github →