Commit 2025-09-15 13:59 44bb47ff

feat(LinearAlgebra): symmetric tensor power (#26192) This file defines the symmetric tensor power of a module over a ring. The finite powers will form a grading of the symmetric algebra. The n-th symmetric R-tensor power of M will also correspond to global sections of a line bundle on Proj(M) of degree n. It also has a universal property where maps out of it correspond to symmetric multilinear forms. We implement the modules separately instead deriving it from the algebra because this way allows us to generalise it to the case where we have an infinite indexing set, which allows us to talk about infinitely multilinear symmetric linear maps.