Perm

📁 Source: Mathlib/Data/Fintype/Perm.lean

Statistics

Metric	Count
Definitions instFintype, instFintype, instFintype, fintypePerm, permsOfFinset, permsOfList	6
Theorems card_equiv, card_perm, card_perms_of_finset, length_permsOfList, mem_of_mem_permsOfList, mem_permsOfList_iff, mem_permsOfList_of_mem, mem_perms_of_finset_iff, nodup_permsOfList	9
Total	15

AddEquiv

Definitions

Name	Category	Theorems
instFintype 📖	CompOp	—

Equiv

Definitions

Name	Category	Theorems
instFintype 📖	CompOp	34 math math: Matrix.det_apply, ContinuousMultilinearMap.alternatization_apply_apply, Perm.card_of_cycleType_mul_eq, AlternatingMap.domCoprod_coe, Fintype.card_perm, Perm.OnCycleFactors.kerParam_range_card, Fintype.card_equiv, Perm.card_of_cycleType_eq_zero_iff, MultilinearMap.domCoprod_alternization_coe, Finset.univ_perm_option, Perm.card_of_cycleType, ContinuousMultilinearMap.iteratedFDeriv_comp_diagonal, DomMulAct.stabilizer_card', MultilinearMap.alternatization_apply, Finset.univ_perm_fin_succ, two_mul_card_alternatingGroup, ContinuousMultilinearMap.alternatization_apply_toContinuousMultilinearMap, Matrix.det_mul_aux, HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_completeSpace, MultilinearMap.alternatization_coe, HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum_of_completeSpace, Matrix.det_apply', Perm.card_of_cycleType_singleton, AlternatingGroup.map_subtype_of_cycleType, Numbering.dens_prefixed, AlternatingMap.domCoprod_apply, Perm.ofSign_disjUnion, exteriorPower.toTensorPower_apply_ιMulti, Fintype.card_numbering, DomMulAct.stabilizer_card, HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum, exists_eq_sum_perm_of_mem_doublyStochastic, HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum, MultilinearMap.alternatization_def

Fintype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_equiv 📖	mathematical	—	card Equiv Equiv.instFintype Nat.factorial	—	card_perm card_congr
card_perm 📖	mathematical	—	card Equiv.Perm Equiv.instFintype Nat.factorial	—	card_perms_of_finset subsingleton

MulEquiv

Definitions

Name	Category	Theorems
instFintype 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
fintypePerm 📖	CompOp	—
permsOfFinset 📖	CompOp	2 math math: card_perms_of_finset, mem_perms_of_finset_iff
permsOfList 📖	CompOp	4 math math: length_permsOfList, mem_permsOfList_of_mem, mem_permsOfList_iff, nodup_permsOfList

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_perms_of_finset 📖	mathematical	—	Finset.card Equiv.Perm permsOfFinset Nat.factorial	—	length_permsOfList
length_permsOfList 📖	mathematical	—	Equiv.Perm permsOfList Nat.factorial	—	List.sum_replicate add_comm
mem_of_mem_permsOfList 📖	—	Equiv.Perm permsOfList	—	—	eq_inv_mul_iff_mul_eq Equiv.Perm.mul_apply Equiv.swap_inv Equiv.swap_apply_def
mem_permsOfList_iff 📖	mathematical	—	Equiv.Perm permsOfList	—	mem_of_mem_permsOfList mem_permsOfList_of_mem
mem_permsOfList_of_mem 📖	mathematical	—	Equiv.Perm permsOfList	—	Equiv.ext Equiv.injective Equiv.swap_apply_right mul_assoc Equiv.Perm.mul_def Equiv.swap_swap Equiv.Perm.one_def one_mul
mem_perms_of_finset_iff 📖	mathematical	—	Equiv.Perm Finset Finset.instMembership permsOfFinset	—	mem_permsOfList_iff
nodup_permsOfList 📖	mathematical	—	Equiv.Perm permsOfList	—	List.Nodup.of_cons mem_of_mem_permsOfList permsOfList.eq_2 List.nodup_append' List.nodup_flatMap List.Nodup.map mul_left_cancel LeftCancelSemigroup.toIsLeftCancelMul Equiv.Perm.mul_apply Equiv.swap_apply_left List.Nodup.getElem_inj_iff ne_of_lt Equiv.apply_symm_apply Equiv.injective Equiv.swap_apply_right

---

← Back to Index