mathlib3

9232032b - refactor(linear_algebra/tensor_algebra): build as a quotient of a free algebra (#4079)