Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-24 19:36 f83ae595

View on Github →

feat(group_theory/nielsen_schreier): subgroup of free group is free (#6840) Prove that a subgroup of a free group is itself free

Estimated changes

Modified src/category_theory/endomorphism.lean

modified def category_theory.functor.map_End

Modified src/category_theory/is_connected.lean

Modified src/category_theory/single_obj.lean

added def category_theory.single_obj.difference_functor

Modified src/combinatorics/quiver.lean

modified def quiver.labelling

modified structure quiver.total

Created src/group_theory/nielsen_schreier.lean

added theorem is_free_groupoid.ext_functor

added def is_free_groupoid.generators

added theorem is_free_groupoid.path_nonempty_of_hom

added def is_free_groupoid.spanning_tree.End_is_free

added def is_free_groupoid.spanning_tree.functor_of_monoid_hom

added def is_free_groupoid.spanning_tree.loop_of_hom

added theorem is_free_groupoid.spanning_tree.loop_of_hom_eq_id

added def is_free_groupoid.spanning_tree.tree_hom

added theorem is_free_groupoid.spanning_tree.tree_hom_eq

added theorem is_free_groupoid.spanning_tree.tree_hom_root