Commit 2023-02-27 13:06 82cc6f65

View on Github →

feat: port GroupTheory.Perm.Sign (#2458)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/GroupTheory/Perm/Basic.lean

Created Mathlib/GroupTheory/Perm/Sign.lean

added theorem Equiv.Perm.Disjoint.extendDomain

added theorem Equiv.Perm.IsSwap.sign_eq

added theorem Equiv.Perm.closure_isSwap

added theorem Equiv.Perm.eq_sign_of_surjective_hom

added def Equiv.Perm.finPairsLT

added theorem Equiv.Perm.isConj_swap

added theorem Equiv.Perm.mem_finPairsLT

added theorem Equiv.Perm.mem_sumCongrHom_range_of_perm_mapsTo_inl

added def Equiv.Perm.modSwap

added theorem Equiv.Perm.perm_inv_mapsTo_iff_mapsTo

added theorem Equiv.Perm.perm_inv_mapsTo_of_mapsTo

added theorem Equiv.Perm.perm_inv_on_of_perm_on_finite

added theorem Equiv.Perm.perm_inv_on_of_perm_on_finset

added theorem Equiv.Perm.perm_mapsTo_inl_iff_mapsTo_inr

added theorem Equiv.Perm.prod_prodExtendRight

added def Equiv.Perm.sign

added def Equiv.Perm.signAux2

added def Equiv.Perm.signAux3

added theorem Equiv.Perm.signAux3_mul_and_swap

added theorem Equiv.Perm.signAux3_symm_trans_trans

added def Equiv.Perm.signAux

added theorem Equiv.Perm.signAux_eq_signAux2

added theorem Equiv.Perm.signAux_inv

added theorem Equiv.Perm.signAux_mul

added theorem Equiv.Perm.signAux_one

added theorem Equiv.Perm.signAux_swap

added def Equiv.Perm.signBijAux

added theorem Equiv.Perm.signBijAux_inj

added theorem Equiv.Perm.signBijAux_mem

added theorem Equiv.Perm.signBijAux_surj

added theorem Equiv.Perm.sign_bij

added theorem Equiv.Perm.sign_eq_sign_of_equiv

added theorem Equiv.Perm.sign_extendDomain

added theorem Equiv.Perm.sign_inv

added theorem Equiv.Perm.sign_mul

added theorem Equiv.Perm.sign_ofSubtype

added theorem Equiv.Perm.sign_one

added theorem Equiv.Perm.sign_permCongr

added theorem Equiv.Perm.sign_prodCongrLeft

added theorem Equiv.Perm.sign_prodCongrRight

added theorem Equiv.Perm.sign_prodExtendRight

added theorem Equiv.Perm.sign_prod_list_swap

added theorem Equiv.Perm.sign_refl

added theorem Equiv.Perm.sign_subtypeCongr

added theorem Equiv.Perm.sign_subtypePerm

added theorem Equiv.Perm.sign_sumCongr

added theorem Equiv.Perm.sign_surjective

added theorem Equiv.Perm.sign_swap'

added theorem Equiv.Perm.sign_swap

added theorem Equiv.Perm.sign_symm

added theorem Equiv.Perm.sign_symm_trans_trans

added theorem Equiv.Perm.sign_trans

added theorem Equiv.Perm.sign_trans_trans_symm

added theorem Equiv.Perm.subtypePermOfFintype_apply

added theorem Equiv.Perm.subtypePermOfFintype_one

added theorem Equiv.Perm.support_pow_coprime

added def Equiv.Perm.swapFactors

added def Equiv.Perm.swapFactorsAux

added theorem Equiv.Perm.swap_induction_on'

added theorem Equiv.Perm.swap_induction_on

added def Equiv.Perm.truncSwapFactors