Commit 2023-05-15 14:58 a39a8f5b

View on Github →

feat: port GroupTheory.NielsenSchreier (#3981)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/NielsenSchreier.lean

added def IsFreeGroupoid.Generators

added def IsFreeGroupoid.SpanningTree.endIsFree

added def IsFreeGroupoid.SpanningTree.functorOfMonoidHom

added def IsFreeGroupoid.SpanningTree.homOfPath

added def IsFreeGroupoid.SpanningTree.loopOfHom

added theorem IsFreeGroupoid.SpanningTree.loopOfHom_eq_id

added def IsFreeGroupoid.SpanningTree.treeHom

added theorem IsFreeGroupoid.SpanningTree.treeHom_eq

added theorem IsFreeGroupoid.SpanningTree.treeHom_root

added theorem IsFreeGroupoid.ext_functor

added theorem IsFreeGroupoid.path_nonempty_of_hom