Commit 2022-05-24 12:33 53a70a08
View on Github →feat(linear_algebra/tensor_power): Add notation for tensor powers, and a definition of multiplication (#14196)
This file introduces the notation ⨂[R]^n M for tensor_power R n M, which in turn is an
abbreviation for ⨂[R] i : fin n, M.
The proof that this multiplication forms a semiring will come in a later PR (#10255).