mathlib3
395d8716 - chore(algebra/lie/free): tidy up after #8153 (#8163)

Commit
4 years ago
chore(algebra/lie/free): tidy up after #8153 (#8163) @eric-wieser had some further comments and suggestions which didn't make it into #8153
References
Author
Parents
Loading