Commit 2022-12-19 15:36 395f1974

View on Github →

feat: port group_theory.perm.basic (#1105)

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Perm/Basic.lean

added theorem Equiv.Perm.apply_inv_self

added theorem Equiv.Perm.coe_mul

added theorem Equiv.Perm.coe_one

added theorem Equiv.Perm.default_eq

added theorem Equiv.Perm.eq_inv_iff_eq

added def Equiv.Perm.equivUnitsEnd

added def Equiv.Perm.extendDomainHom

added theorem Equiv.Perm.extendDomainHom_injective

added theorem Equiv.Perm.extendDomain_eq_one_iff

added theorem Equiv.Perm.extendDomain_inv

added theorem Equiv.Perm.extendDomain_mul

added theorem Equiv.Perm.extendDomain_one

added theorem Equiv.Perm.inv_apply_self

added theorem Equiv.Perm.inv_def

added theorem Equiv.Perm.inv_eq_iff_eq

added theorem Equiv.Perm.inv_subtypePerm

added theorem Equiv.Perm.inv_trans_self

added theorem Equiv.Perm.iterate_eq_pow

added theorem Equiv.Perm.mem_iff_ofSubtype_apply_mem

added theorem Equiv.Perm.mul_apply

added theorem Equiv.Perm.mul_def

added theorem Equiv.Perm.mul_refl

added theorem Equiv.Perm.mul_symm

added def Equiv.Perm.ofSubtype

added theorem Equiv.Perm.ofSubtype_apply_coe

added theorem Equiv.Perm.ofSubtype_apply_of_mem

added theorem Equiv.Perm.ofSubtype_apply_of_not_mem

added theorem Equiv.Perm.ofSubtype_subtypePerm

added theorem Equiv.Perm.one_apply

added theorem Equiv.Perm.one_def

added theorem Equiv.Perm.one_symm

added theorem Equiv.Perm.one_trans

added theorem Equiv.Perm.permCongr_eq_mul

added theorem Equiv.Perm.refl_inv

added theorem Equiv.Perm.refl_mul

added theorem Equiv.Perm.self_trans_inv

added def Equiv.Perm.sigmaCongrRightHom

added theorem Equiv.Perm.sigmaCongrRightHom_injective

added theorem Equiv.Perm.sigmaCongrRight_inv

added theorem Equiv.Perm.sigmaCongrRight_mul

added theorem Equiv.Perm.sigmaCongrRight_one

added def Equiv.Perm.subtypeCongrHom

added theorem Equiv.Perm.subtypeCongrHom_injective

added theorem Equiv.Perm.subtypeEquivSubtypePerm_apply_of_mem

added theorem Equiv.Perm.subtypeEquivSubtypePerm_apply_of_not_mem

added def Equiv.Perm.subtypePerm

added theorem Equiv.Perm.subtypePerm_apply

added theorem Equiv.Perm.subtypePerm_inv

added theorem Equiv.Perm.subtypePerm_mul

added theorem Equiv.Perm.subtypePerm_ofSubtype

added theorem Equiv.Perm.subtypePerm_one

added theorem Equiv.Perm.subtypePerm_pow

added theorem Equiv.Perm.subtypePerm_zpow

added def Equiv.Perm.sumCongrHom

added theorem Equiv.Perm.sumCongrHom_injective

added theorem Equiv.Perm.sumCongr_inv

added theorem Equiv.Perm.sumCongr_mul

added theorem Equiv.Perm.sumCongr_one

added theorem Equiv.Perm.sumCongr_one_swap

added theorem Equiv.Perm.sumCongr_swap_one

added theorem Equiv.Perm.symm_mul

added theorem Equiv.Perm.trans_one

added theorem Equiv.Perm.zpow_apply_comm

added theorem Equiv.mul_swap_eq_iff

added theorem Equiv.mul_swap_eq_swap_mul

added theorem Equiv.mul_swap_involutive

added theorem Equiv.mul_swap_mul_self

added theorem Equiv.swap_apply_apply

added theorem Equiv.swap_eq_one_iff

added theorem Equiv.swap_inv

added theorem Equiv.swap_mul_eq_iff

added theorem Equiv.swap_mul_eq_mul_swap

added theorem Equiv.swap_mul_involutive

added theorem Equiv.swap_mul_self

added theorem Equiv.swap_mul_self_mul

added theorem Equiv.swap_mul_swap_mul_swap

added def MonoidHom.toHomPerm