Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-11 20:49 57a8933b

View on Github →

feat(group_theory/free_group): promote free_group_congr to a mul_equiv (#11373) Also some various golfs and cleanups

Estimated changes

Modified src/group_theory/free_group.lean

modified def free_group.free_group_congr

added theorem free_group.free_group_congr_refl

added theorem free_group.free_group_congr_symm

added theorem free_group.free_group_congr_trans

deleted def free_group.map.aux

modified theorem free_group.map.comp

modified theorem free_group.map.id'

modified theorem free_group.map.id

deleted def free_group.map.to_fun

modified def free_group.map

added theorem free_group.quot_map_mk