Theorem PiTensorProduct.map_one

Modification history

2025-03-29 19:12
Mathlib/LinearAlgebra/PiTensorProduct.lean
refactor: protect `map_mul` lemmas (#23403) …
Deleted PiTensorProduct.map_oneView on Github →
2024-03-08 09:46
Mathlib/LinearAlgebra/PiTensorProduct.lean
feat(LinearAlgebra/PiTensorProduct): some more functoriality properties of `PiTensorProduct` (#11152) …
Added PiTensorProduct.map_oneView on Github →