feat(linear_algebra/tensor_algebra): Tensor algebras (#3531)
This PR constructs the tensor algebra of a module over a commutative ring.
The main components are:
1. The construction of the tensor algebra: `tensor_algebra R M` for a module `M` over a commutative ring `R`.
2. The linear map `univ R M` from `M` to `tensor_algebra R M`.
3. Given a linear map `f`from `M`to an `R`-algebra `A`, the lift of `f` to `tensor_algebra R M` is denoted `lift R M f`.
4. A theorem `univ_comp_lift` asserting that the composition of `univ R M` with `lift R M f`is `f`.
5. A theorem `lift_unique` asserting the uniqueness of `lift R M f`with respect to property 4.
Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
