mathlib3

53a70a08 - feat(linear_algebra/tensor_power): Add notation for tensor powers, and a definition of multiplication (#14196)

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).