Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-22 18:38 155cf1df

View on Github →

feat(group_theory/abelianization): add mul_equiv.abelianization_congr (#11466)

Estimated changes

Modified src/group_theory/abelianization.lean

added theorem abelianization.lift_of

added def abelianization.map

added theorem abelianization.map_comp

added theorem abelianization.map_id

added theorem abelianization.map_map_apply

added theorem abelianization.map_of

added theorem abelianization.mk_eq_of

added theorem abelianization_congr_of

added theorem abelianization_congr_refl

added theorem abelianization_congr_symm

added theorem abelianization_congr_trans

added def mul_equiv.abelianization_congr