Def SymmetricPower.tprod

Modification history

2026-10-29 21:19

Mathlib/LinearAlgebra/TensorPower/Symmetric.lean

feat(LinearAlgebra/MultilinearMap): notation for `MultilinearMap` (#43877) …

Modified SymmetricPower.tprod View on Github →

2025-09-15 13:59

Mathlib/LinearAlgebra/TensorPower/Symmetric.lean

feat(LinearAlgebra): symmetric tensor power (#26192) …

Added SymmetricPower.tprod View on Github →