mathlib3

d97a0c9f - feat(linear_algebra/tensor_power): the tensor powers form a graded algebra (#10255)