Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-04 18:03 6d153f1b

View on Github →

feat(data/equiv/basic): perm.subtype_congr (#5875)

Estimated changes

Modified src/data/equiv/basic.lean

added theorem equiv.perm.subtype_congr.apply

added theorem equiv.perm.subtype_congr.left_apply

added theorem equiv.perm.subtype_congr.left_apply_subtype

added theorem equiv.perm.subtype_congr.refl

added theorem equiv.perm.subtype_congr.right_apply

added theorem equiv.perm.subtype_congr.right_apply_subtype

added theorem equiv.perm.subtype_congr.symm

added theorem equiv.perm.subtype_congr.trans

added def equiv.perm.subtype_congr

Modified src/group_theory/perm/basic.lean

added def equiv.perm.subtype_congr_hom

added theorem equiv.perm.subtype_congr_hom_injective

Modified src/group_theory/perm/sign.lean

added theorem equiv.perm.sign_subtype_congr

Modified src/group_theory/perm/subgroup.lean

added theorem equiv.perm.subtype_congr_hom.card_range