mathlib3

34ebade1 - feat(algebra/free_algebra): free (noncommutative) algebras (#4077)

feat(algebra/free_algebra): free (noncommutative) algebras (#4077) Previously, @adamtopaz constructed the tensor algebra of an `R`-module via a direct construction of a quotient of a free algebra. This uses essentially the same construction to build a free algebra (on a type) directly. In a PR coming shortly, I'll refactor his development of the tensor algebra to use this construction. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>