Mathlib Changelog
v4
Changelog
About
Github
Theorem
FreeGroup.startsWith.Injective
Modification history
2025-10-23 13:34
Mathlib/GroupTheory/FreeGroup/Orbit.lean
feat(GroupTheory/FreeGroup/Orbit): The orbit of a point generated by parts of a free group can be "duplicated" (#30130) …
Added
FreeGroup.startsWith.Injective
View on Github →