Commit 2022-04-02 13:47 1d5b99b2
View on Github →feat(group_theory/free_product): add (m)range_eq_supr (#12956)
and lemmas leading to it as inspired by the corresponding lemmas from
free_groups.lean.
As suggested by @ocfnash, polish the free group lemmas a bit as well.