feat(group_theory/free_group): norm of elements (#15503)
This PR adds to a new `free_group.metric` namespace some useful lemmas related to the word metric on the free group. This will be useful for defining the word metric for an arbitrary (marked) group.
Co-authored-by: Jim Fowler <fowler@math.osu.edu>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Oliver Nash <github@olivernash.org>
