Def PiTensorProduct.tmulEquiv
Modification history
2025-04-30 12:12
Mathlib/LinearAlgebra/PiTensorProduct.lean
feat(LinearAlgebra/PiTensorProduct): dependent version of tmulEquiv (#18534) …
Modified PiTensorProduct.tmulEquivView on Github →2024-07-20 07:03
Mathlib/LinearAlgebra/PiTensorProduct.lean
chore(*): use ⊕ notation for `Sum` (#14934)
Modified PiTensorProduct.tmulEquivView on Github →