mathlib

be05d53c - feat(algebra/free_monoid): add 2 lemmas (#16712)