Theorem PiTensorProduct.span_tprod_eq_top

Modification history

2024-03-08 09:46
Mathlib/LinearAlgebra/PiTensorProduct.lean
feat(LinearAlgebra/PiTensorProduct): some more functoriality properties of `PiTensorProduct` (#11152) …
Added PiTensorProduct.span_tprod_eq_topView on Github →