mathlib3

5f328b6e - feat(linear_algebra/free_algebra): Show that free_monoid forms a basis over free_algebra (#5868)