Commit 2022-05-04 15:53 923ae0bc

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.