Commit 2023-01-27 17:43 1190327d

View on Github →

feat: port GroupTheory.IsFreeGroup (#1889)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/IsFreeGroup.lean

added def IsFreeGroup.MulEquiv

added theorem IsFreeGroup.ext_hom

added theorem IsFreeGroup.lift'_eq_freeGroup_lift

added def IsFreeGroup.lift

added theorem IsFreeGroup.lift_of

added theorem IsFreeGroup.lift_symm_apply

added def IsFreeGroup.of

added def IsFreeGroup.ofLift

added def IsFreeGroup.ofMulEquiv

added theorem IsFreeGroup.of_eq_freeGroup_of

added def IsFreeGroup.toFreeGroup

added theorem IsFreeGroup.unique_lift