mathlib3

923ae0bc - feat(group_theory/free_group): is_free_group via `free_group X ≃* G` (#13633)

feat(group_theory/free_group): is_free_group via `free_group X ≃* G` (#13633) The previous definition of the `is_free_group` class was defined via the universal property of free groups, which is intellectually pleasing, but technically annoying, due to the universe problems of quantifying over “all other groups” in the definition. To work around them, many definitions had to be duplicated. This changes the definition of `is_free_group` to contain an isomorphism between the `free_group` over the generator and `G`. It also moves this class into `free_group.lean`, so that it can be found more easily. Relevant Zulip thread: <https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/universe.20levels.20for.20is_free_group> A previous attempt at reforming `is_free_group` to unbundle the set of generators (`is_freely_generated_by G X`) is on branch `joachim/is_freely_generated_by`, but it wasn't very elegant to use in some places.