Sign

📁 Source: Mathlib/GroupTheory/Perm/Sign.lean

Statistics

Metric	Count
Definitions finPairsLT, instDecidableRelROfFintype, modSwap, ofSign, sign, signAux, signAux2, signAux3, signBijAux, swapFactors, swapFactorsAux, truncSwapFactors	12
Theorems sign_eq, closure_isSwap, eq_sign_of_surjective_hom, isConj_swap, mclosure_isSwap, mclosure_swap_castSucc_succ, mem_finPairsLT, mem_ofSign, ofSign_disjUnion, ofSign_disjoint, prod_prodExtendRight, signAux3_mul_and_swap, signAux3_symm_trans_trans, signAux_eq_signAux2, signAux_inv, signAux_mul, signAux_one, signAux_swap, signBijAux_injOn, signBijAux_mem, signBijAux_surj, sign_abs, sign_bij, sign_eq_sign_of_equiv, sign_extendDomain, sign_inv, sign_mul, sign_ofSubtype, sign_one, sign_permCongr, sign_prodCongrLeft, sign_prodCongrRight, sign_prodExtendRight, sign_prod_list_swap, sign_refl, sign_subtypeCongr, sign_subtypePerm, sign_sumCongr, sign_surjective, sign_swap, sign_swap', sign_symm, sign_symm_trans_trans, sign_trans, sign_trans_trans_symm, swap_induction_on, swap_induction_on', viaFintypeEmbedding_sign	48
Total	60

Equiv.Perm

Definitions

Name	Category	Theorems
finPairsLT 📖	CompOp	2 math math: mem_finPairsLT, signBijAux_injOn
instDecidableRelROfFintype 📖	CompOp	—
modSwap 📖	CompOp	—
ofSign 📖	CompOp	4 math math: Matrix.adjp_apply, ofSign_disjoint, mem_ofSign, ofSign_disjUnion
sign 📖	CompOp	69 math math: Fin.sign_cycleIcc_of_eq, AlternatingMap.domCoprod.summand_mk'', Matrix.det_apply, ContinuousMultilinearMap.alternatization_apply_apply, AlternatingMap.map_perm, sign_of_cycleType, Matrix.det_permute, sign_subtypePerm, sign_trans_trans_symm, viaFintypeEmbedding_sign, sign_symm, Fin.sign_cycleRange, sign_eq_prod_prod_Ioi, prod_Ioi_comp_eq_sign_mul_prod, alternatingGroup.normalClosure_swap_mul_swap_five, sign_of_cycleType_eq_replicate, decomposeFin.symm_sign, AlternatingMap.map_congr_perm, sign_prodExtendRight, sign_abs, Fin.sign_cycleIcc_of_ge, MultilinearMap.domCoprod_alternization_coe, sign_trans, sign_sumCongr, sign_eq_prod_prod_Iio, Matrix.det_permutation, NumberField.InfinitePlace.ComplexEmbedding.conjugate_sign, sign_bij, Fin.sign_cycleIcc_of_le, mem_alternatingGroup, Matrix.det_reindex, sign_of_pow_two_eq_one, sign_refl, sign_mul, sign_symm_trans_trans, mem_ofSign, MultilinearMap.alternatization_apply, decomposeOption_symm_sign, sign_permCongr, ContinuousMultilinearMap.alternatization_apply_toContinuousMultilinearMap, Matrix.det_mul_aux, Matrix.det_permute', MultilinearMap.alternatization_coe, sign_extendDomain, sign_finRotate, eq_sign_of_surjective_hom, IsCycle.sign, sign_inv, IsThreeCycle.sign, AlternatingMap.domDomCongr_perm, IsSwap.sign_eq, sign_prodCongrRight, sign_eq_sign_of_equiv, sign_one, Matrix.det_apply', sign_prod_list_swap, sign_prodCongrLeft, sign_of_cycleType', sign_subtypeCongr, exteriorPower.toTensorPower_apply_ιMulti, prod_Iio_comp_eq_sign_mul_prod, alternatingGroup_eq_sign_ker, Equiv.optionCongr_sign, sign_swap', sign_swap, sign_ofSubtype, MultilinearMap.alternatization_def, sign_surjective, OnCycleFactors.sign_kerParam_apply_apply
signAux 📖	CompOp	5 math math: signAux_swap, signAux_inv, signAux_one, signAux_eq_signAux2, signAux_mul
signAux2 📖	CompOp	1 math math: signAux_eq_signAux2
signAux3 📖	CompOp	2 math math: signAux3_symm_trans_trans, signAux3_mul_and_swap
signBijAux 📖	CompOp	3 math math: signBijAux_surj, signBijAux_mem, signBijAux_injOn
swapFactors 📖	CompOp	—
swapFactorsAux 📖	CompOp	—
truncSwapFactors 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closure_isSwap 📖	mathematical	—	Subgroup.closure Equiv.Perm permGroup setOf IsSwap Top.top Subgroup Subgroup.instTop	—	Subgroup.closure_eq_top_of_mclosure_eq_top mclosure_isSwap
eq_sign_of_surjective_hom 📖	mathematical	Equiv.Perm Units Int.instMonoid DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike	sign	—	by_contradiction isConj_iff_eq Int.units_eq_one_or MonoidHom.map_isConj isConj_swap List.prod_hom MonoidHom.instMonoidHomClass List.eq_replicate_length List.prod_replicate one_pow IsSwap.congr_simp MonoidHom.ext sign_prod_list_swap
isConj_swap 📖	mathematical	—	IsConj Equiv.Perm DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Equiv.swap	—	isConj_iff mul_inv_rev Equiv.swap_inv mul_assoc Equiv.swap_mul_swap_mul_swap Equiv.swap_comm
mclosure_isSwap 📖	mathematical	—	Submonoid.closure Equiv.Perm Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup setOf IsSwap Top.top Submonoid Submonoid.instTop	—	nonempty_fintype top_unique Subtype.mem Submonoid.list_prod_mem Submonoid.subset_closure
mclosure_swap_castSucc_succ 📖	mathematical	—	Submonoid.closure Equiv.Perm Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Set.range Equiv.swap Top.top Submonoid Submonoid.instTop	—	top_unique mclosure_isSwap Finite.of_fintype Submonoid.closure_le Submonoid.subset_closure LE.le.eq_or_lt Equiv.swap_comm Equiv.swap_mul_swap_mul_swap LT.lt.ne MulMemClass.mul_mem SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass Ne.lt_or_gt
mem_finPairsLT 📖	mathematical	—	Finset Finset.instMembership finPairsLT	—	—
mem_ofSign 📖	mathematical	—	Equiv.Perm Finset Finset.instMembership ofSign DFunLike.coe MonoidHom Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign	—	ofSign.eq_1 Finset.mem_filter Finset.mem_univ
ofSign_disjUnion 📖	mathematical	—	Finset.disjUnion Equiv.Perm ofSign Units Int.instMonoid Units.instOne Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing ofSign_disjoint Finset.univ Equiv.instFintype	—	Finset.ext ofSign_disjoint
ofSign_disjoint 📖	mathematical	—	Disjoint Finset Equiv.Perm Finset.partialOrder Finset.instOrderBot ofSign Units Int.instMonoid Units.instOne Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	Finset.disjoint_iff_ne mem_ofSign
prod_prodExtendRight 📖	mathematical	—	Equiv.Perm instMul instOne prodExtendRight Equiv.prodCongrRight	—	ext one_apply mul_apply prodExtendRight_apply_ne prodExtendRight_apply_eq Equiv.prodCongrRight_apply
signAux3_mul_and_swap 📖	mathematical	Multiset Multiset.instMembership	signAux3 Equiv.Perm instMul Units Int.instMonoid Units.instMul Pairwise Equiv.swap Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Units.instOne	—	Finite.exists_equiv_fin Equiv.ext Equiv.symm_apply_apply signAux_eq_signAux2 signAux_mul Equiv.symm_trans_swap_trans signAux_swap Equiv.injective
signAux3_symm_trans_trans 📖	mathematical	Multiset Multiset.instMembership	signAux3 Equiv.trans Equiv.symm	—	Finite.exists_equiv_fin signAux_eq_signAux2 Equiv.ext
signAux_eq_signAux2 📖	mathematical	—	signAux Equiv.trans Equiv.symm signAux2	—	Equiv.ext one_def Equiv.trans_refl Equiv.symm_trans_self signAux_one signAux2.eq_1 signAux2.eq_2 ne_and_ne_of_swap_mul_apply_ne_self ext Equiv.symm_trans_swap_trans mul_def Equiv.trans_apply EquivLike.toEmbeddingLike Equiv.injective signAux_mul signAux_swap neg_mul one_mul neg_neg
signAux_inv 📖	mathematical	—	signAux Equiv.Perm instInv	—	Finset.prod_nbij signBijAux_mem signBijAux_injOn signBijAux_surj Equiv.apply_symm_apply LT.lt.not_ge mem_finPairsLT LT.lt.le
signAux_mul 📖	mathematical	—	signAux Equiv.Perm instMul Units Int.instMonoid Units.instMul	—	signAux_inv Finset.prod_mul_distrib Finset.prod_nbij signBijAux_mem signBijAux_injOn signBijAux_surj mul_apply Equiv.symm_apply_apply mul_ite mul_neg mul_one mem_finPairsLT Ne.lt_or_gt Equiv.injective LT.lt.ne neg_neg
signAux_one 📖	mathematical	—	signAux Equiv.Perm instOne Units Int.instMonoid Units.instOne	—	Finset.prod_const_one Finset.prod_congr LT.lt.not_ge mem_finPairsLT
signAux_swap 📖	mathematical	—	signAux Equiv.swap Units Int.instMonoid Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Units.instOne	—	Finset.prod_congr Finset.prod_const instIsEmptyFalse le_add_self Nat.instCanonicallyOrderedAdd isConj_iff_eq lt_of_lt_of_le MonoidHom.map_isConj signAux_mul isConj_swap
signBijAux_injOn 📖	mathematical	—	Set.InjOn signBijAux SetLike.coe Finset Finset.instSetLike finPairsLT	—	LE.le.not_gt LT.lt.le mem_finPairsLT Finset.mem_coe Equiv.injective not_le
signBijAux_mem 📖	mathematical	Finset Finset.instMembership finPairsLT	signBijAux	—	mem_finPairsLT LE.le.lt_of_ne le_of_not_gt LT.lt.ne Equiv.injective
signBijAux_surj 📖	mathematical	Finset Finset.instMembership finPairsLT	signBijAux	—	mem_finPairsLT Equiv.apply_symm_apply LE.le.lt_of_ne le_of_not_gt Equiv.injective LE.le.not_gt LT.lt.le
sign_abs 📖	mathematical	—	abs instLatticeInt Int.instAddGroup Units.val Int.instMonoid DFunLike.coe MonoidHom Equiv.Perm Units MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign	—	Int.abs_eq_natAbs Int.units_natAbs Nat.cast_one
sign_bij 📖	mathematical	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	MonoidHom Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign	—	EquivLike.toEmbeddingLike sign_subtypePerm sign_eq_sign_of_equiv Equiv.injective
sign_eq_sign_of_equiv 📖	mathematical	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.Perm	MonoidHom Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign	—	Equiv.ext Equiv.apply_symm_apply sign_symm_trans_trans
sign_extendDomain 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign extendDomain	—	sign_subtypeCongr sign_permCongr sign_refl mul_one
sign_inv 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign instInv	—	map_inv MonoidHom.instMonoidHomClass Int.units_inv_eq_self
sign_mul 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign instMul Units.instMul	—	map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass
sign_ofSubtype 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign ofSubtype Subtype.fintype	—	sign_extendDomain
sign_one 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign instOne Units.instOne	—	map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass
sign_permCongr 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.permCongr	—	sign_eq_sign_of_equiv Equiv.symm_apply_apply
sign_prodCongrLeft 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign instFintypeProd Equiv.prodCongrLeft Finset.prod CommGroup.toCommMonoid Units.instCommGroupUnits Int.instCommMonoid Finset.univ	—	sign_eq_sign_of_equiv sign_prodCongrRight
sign_prodCongrRight 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign instFintypeProd Equiv.prodCongrRight Finset.prod CommGroup.toCommMonoid Units.instCommGroupUnits Int.instCommMonoid Finset.univ	—	Finite.exists_univ_list Finite.of_fintype eq_top_iff List.mem_toFinset prod_prodExtendRight map_list_prod MonoidHom.instMonoidHomClass List.prod_toFinset sign_prodExtendRight
sign_prodExtendRight 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign instFintypeProd prodExtendRight	—	sign_bij eq_of_prodExtendRight_ne prodExtendRight_apply_eq
sign_prod_list_swap 📖	mathematical	IsSwap	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign instMul instOne Monoid.toNatPow Units.instMonoid Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Units.instOne	—	IsSwap.sign_eq List.prod_replicate List.prod_hom MonoidHom.instMonoidHomClass
sign_refl 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign Equiv.refl Units.instOne	—	map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass
sign_subtypeCongr 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign subtypeCongr Units.instMul Subtype.fintype	—	sign_permCongr sign_sumCongr
sign_subtypePerm 📖	mathematical	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	MonoidHom Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign Subtype.fintype subtypePerm	—	IsSwap.of_subtype_isSwap List.prod_hom MonoidHom.instMonoidHomClass ofSubtype_subtypePerm sign_prod_list_swap
sign_sumCongr 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign instFintypeSum sumCongr Units.instMul	—	swap_induction_on Finite.of_fintype sumCongr_one sign_one one_mul sumCongr_mul sign_mul sumCongr_swap_one sign_swap Sum.inl_injective sumCongr_one_swap Sum.inr_injective mul_one
sign_surjective 📖	mathematical	—	Equiv.Perm Units Int.instMonoid DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign	—	Int.units_eq_one_or sign_one exists_pair_ne sign_swap
sign_swap 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign Equiv.swap Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Units.instOne	—	Finite.of_fintype Finset.mem_univ signAux3_mul_and_swap
sign_swap' 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign Equiv.swap Units.instOne Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	Equiv.swap_self sign_refl sign_swap
sign_symm 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign Equiv.symm	—	sign_inv
sign_symm_trans_trans 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign Equiv.trans Equiv.symm	—	signAux3_symm_trans_trans Finite.of_fintype Finset.mem_univ
sign_trans 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign Equiv.trans Units.instMul	—	mul_def sign_mul
sign_trans_trans_symm 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign Equiv.trans Equiv.symm	—	sign_symm_trans_trans
swap_induction_on 📖	—	Equiv.Perm instOne instMul Equiv.swap	—	—	nonempty_fintype
swap_induction_on' 📖	—	Equiv.Perm instOne instMul Equiv.swap	—	—	swap_induction_on inv_inv
viaFintypeEmbedding_sign 📖	mathematical	—	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid permGroup Units.instMulOneClass MonoidHom.instFunLike sign viaFintypeEmbedding	—	sign_extendDomain

Equiv.Perm.IsSwap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sign_eq 📖	mathematical	Equiv.Perm.IsSwap	DFunLike.coe MonoidHom Equiv.Perm Units Int.instMonoid MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Equiv.Perm.permGroup Units.instMulOneClass MonoidHom.instFunLike Equiv.Perm.sign Units.instNeg NonUnitalNonAssocRing.toHasDistribNeg NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing Units.instOne	—	Equiv.Perm.sign_swap

---

← Back to Index