List

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

Statistics

Metric	Count
Definitions formPerm	1
Theorems formPerm_append_pair, formPerm_apply_getElem, formPerm_apply_getElem_length, formPerm_apply_getElem_zero, formPerm_apply_getLast, formPerm_apply_head, formPerm_apply_lt_getElem, formPerm_apply_mem_eq_self_iff, formPerm_apply_mem_ne_self_iff, formPerm_apply_mem_of_mem, formPerm_apply_of_notMem, formPerm_cons_concat_apply_last, formPerm_cons_cons, formPerm_eq_formPerm_iff, formPerm_eq_head_iff_eq_getLast, formPerm_eq_of_isRotated, formPerm_eq_one_iff, formPerm_eq_self_of_notMem, formPerm_ext_iff, formPerm_mem_iff_mem, formPerm_nil, formPerm_pair, formPerm_pow_apply_getElem, formPerm_pow_apply_head, formPerm_pow_length_eq_one_of_nodup, formPerm_reverse, formPerm_rotate, formPerm_rotate_one, formPerm_singleton, form_perm_zpow_apply_mem_imp_mem, mem_of_formPerm_apply_mem, mem_of_formPerm_apply_ne, mem_of_formPerm_ne_self, mem_or_mem_of_zipWith_swap_prod_ne, support_formPerm_le, support_formPerm_le', support_formPerm_of_nodup, support_formPerm_of_nodup', zipWith_swap_prod_support, zipWith_swap_prod_support'	40
Total	41

List

Definitions

Name	Category	Theorems
formPerm 📖	CompOp	46 math math: Equiv.Perm.toList_formPerm_singleton, support_formPerm_le, form_perm_zpow_apply_mem_imp_mem, formPerm_singleton, Cycle.formPerm_coe, formPerm_apply_mem_of_mem, formPerm_apply_getElem_zero, formPerm_apply_getElem, formPerm_apply_getElem_length, formPerm_pair, Nodup.isCycleOn_formPerm, Equiv.Perm.toList_formPerm_isRotated_self, formPerm_pow_apply_head, support_formPerm_of_nodup, Equiv.Perm.formPerm_toList, formPerm_pow_apply_getElem, Equiv.Perm.toList_formPerm_nontrivial, formPerm_mem_iff_mem, formPerm_apply_mem_eq_self_iff, cycleType_formPerm, support_formPerm_le', Equiv.Perm.toList_formPerm_nil, formPerm_apply_of_notMem, formPerm_apply_head, formPerm_pow_length_eq_one_of_nodup, formPerm_apply_lt_getElem, formPerm_eq_one_iff, formPerm_cons_cons, formPerm_eq_head_iff_eq_getLast, pairwise_sameCycle_formPerm, formPerm_rotate_one, formPerm_eq_formPerm_iff, formPerm_apply_getLast, formPerm_reverse, support_formPerm_of_nodup', formPerm_rotate, formPerm_eq_self_of_notMem, formPerm_ext_iff, cycleOf_formPerm, formPerm_cons_concat_apply_last, formPerm_apply_mem_eq_next, formPerm_eq_of_isRotated, formPerm_disjoint_iff, formPerm_append_pair, formPerm_nil, isCycle_formPerm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
formPerm_append_pair 📖	mathematical	—	formPerm Equiv.Perm Equiv.Perm.instMul Equiv.swap	—	mul_assoc LeftCancelSemigroup.toIsLeftCancelMul
formPerm_apply_getElem 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike formPerm LE.le.trans_lt Nat.instPreorder	—	LE.le.trans_lt Nat.instCanonicallyOrderedAdd LE.le.eq_or_lt formPerm_apply_getElem_length formPerm_apply_lt_getElem IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le
formPerm_apply_getElem_length 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike formPerm	—	formPerm_apply_getLast
formPerm_apply_getElem_zero 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike formPerm	—	Nat.instCanonicallyOrderedAdd zero_add formPerm_apply_head
formPerm_apply_getLast 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike formPerm	—	formPerm_cons_concat_apply_last
formPerm_apply_head 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike formPerm	—	formPerm_apply_of_notMem Nodup.notMem Equiv.swap_apply_left
formPerm_apply_lt_getElem 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike formPerm	—	zero_add formPerm_apply_getElem_zero Nat.instCanonicallyOrderedAdd formPerm_singleton Equiv.Perm.one_apply IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nodup.of_cons Equiv.swap_apply_of_ne_of_ne
formPerm_apply_mem_eq_self_iff 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike formPerm	—	LE.le.trans_lt formPerm_apply_getElem Nodup.getElem_inj_iff LT.lt.not_ge LT.lt.trans_le Eq.le LE.le.eq_or_lt covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd LT.lt.ne
formPerm_apply_mem_ne_self_iff 📖	—	—	—	—	formPerm_apply_mem_eq_self_iff not_le
formPerm_apply_mem_of_mem 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike formPerm	—	formPerm_cons_cons Equiv.Perm.mul_apply Equiv.swap_apply_def formPerm_apply_of_notMem Equiv.swap_apply_left
formPerm_apply_of_notMem 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike formPerm	—	not_imp_comm mem_of_formPerm_apply_ne
formPerm_cons_concat_apply_last 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike formPerm	—	mul_one Equiv.swap_apply_right
formPerm_cons_cons 📖	mathematical	—	formPerm Equiv.Perm Equiv.Perm.instMul Equiv.swap	—	—
formPerm_eq_formPerm_iff 📖	mathematical	—	formPerm IsRotated	—	Nat.instCanonicallyOrderedAdd IsRotated.perm zero_add formPerm_eq_one_iff covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le formPerm_ext_iff
formPerm_eq_head_iff_eq_getLast 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike formPerm	—	formPerm_apply_getLast Equiv.injective
formPerm_eq_of_isRotated 📖	mathematical	IsRotated	formPerm	—	formPerm_rotate
formPerm_eq_one_iff 📖	mathematical	—	formPerm Equiv.Perm Equiv.Perm.instOne	—	Nat.instCanonicallyOrderedAdd formPerm_apply_mem_eq_self_iff covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le
formPerm_eq_self_of_notMem 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike formPerm	—	formPerm_apply_of_notMem
formPerm_ext_iff 📖	mathematical	—	formPerm IsRotated	—	Set.mem_setOf_eq Equiv.Perm.ext_iff formPerm_apply_head toFinset_cons Finset.coe_insert coe_toFinset support_formPerm_le' dedup_eq_self card_toFinset support_formPerm_of_nodup' length_rotate LE.le.trans_lt getElem_rotate zero_add LT.lt.trans formPerm_apply_getElem add_right_comm formPerm_eq_of_isRotated
formPerm_mem_iff_mem 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike formPerm	—	mem_of_formPerm_apply_mem formPerm_apply_mem_of_mem
formPerm_nil 📖	mathematical	—	formPerm Equiv.Perm Equiv.Perm.instOne	—	—
formPerm_pair 📖	mathematical	—	formPerm Equiv.swap	—	—
formPerm_pow_apply_getElem 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.Perm.instPowNat formPerm LE.le.trans_lt Nat.instPreorder	—	LE.le.trans_lt add_zero pow_zero pow_succ' formPerm_apply_getElem
formPerm_pow_apply_head 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.Perm.instPowNat formPerm	—	LE.le.trans_lt zero_add formPerm_pow_apply_getElem
formPerm_pow_length_eq_one_of_nodup 📖	mathematical	—	Equiv.Perm Equiv.Perm.instPowNat formPerm Equiv.Perm.instOne	—	Equiv.Perm.ext LE.le.trans_lt formPerm_pow_apply_getElem Equiv.Perm.set_support_zpow_subset coe_toFinset support_formPerm_le'
formPerm_reverse 📖	mathematical	—	formPerm Equiv.Perm Equiv.Perm.instInv	—	formPerm_append_pair Equiv.swap_comm mul_inv_rev
formPerm_rotate 📖	mathematical	—	formPerm	—	rotate_zero rotate_rotate formPerm_rotate_one IsRotated.nodup_iff IsRotated.forall
formPerm_rotate_one 📖	mathematical	—	formPerm	—	Equiv.Perm.ext LE.le.trans_lt formPerm_apply_getElem length_rotate getElem_rotate formPerm_apply_of_notMem
formPerm_singleton 📖	mathematical	—	formPerm Equiv.Perm Equiv.Perm.instOne	—	—
form_perm_zpow_apply_mem_imp_mem 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike DivInvMonoid.toZPow Group.toDivInvMonoid Equiv.Perm.permGroup formPerm	—	Equiv.Perm.set_support_zpow_subset Equiv.Perm.set_support_apply_mem coe_toFinset support_formPerm_le'
mem_of_formPerm_apply_mem 📖	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike formPerm	—	—	Mathlib.Tactic.Contrapose.contrapose₁ formPerm_apply_of_notMem
mem_of_formPerm_apply_ne 📖	—	—	—	—	mem_or_mem_of_zipWith_swap_prod_ne
mem_of_formPerm_ne_self 📖	—	—	—	—	mem_of_formPerm_apply_ne
mem_or_mem_of_zipWith_swap_prod_ne 📖	—	—	—	—	instIsEmptyFalse Equiv.eq_or_eq_of_swap_apply_ne_self
support_formPerm_le 📖	mathematical	—	Finset Preorder.toLE PartialOrder.toPreorder Finset.partialOrder Equiv.Perm.support formPerm toFinset	—	coe_toFinset support_formPerm_le'
support_formPerm_le' 📖	mathematical	—	Set Set.instLE setOf DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike formPerm SetLike.coe Finset Finset.instSetLike toFinset	—	LE.le.trans zipWith_swap_prod_support' Finset.coe_union coe_toFinset Set.instReflSubset tail_subset
support_formPerm_of_nodup 📖	mathematical	—	Equiv.Perm.support formPerm toFinset	—	support_formPerm_of_nodup'
support_formPerm_of_nodup' 📖	mathematical	—	setOf DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike formPerm SetLike.coe Finset Finset.instSetLike toFinset	—	le_antisymm support_formPerm_le' Set.mem_setOf_eq LE.le.trans_lt formPerm_apply_getElem LE.le.eq_or_lt Function.Injective.eq_1 nodup_iff_injective_get
zipWith_swap_prod_support 📖	mathematical	—	Finset Preorder.toLE PartialOrder.toPreorder Finset.partialOrder Equiv.Perm.support Equiv.Perm Equiv.Perm.instMul Equiv.Perm.instOne Equiv.swap SemilatticeSup.toMax Lattice.toSemilatticeSup Finset.instLattice toFinset	—	Finset.coe_union coe_toFinset zipWith_swap_prod_support'
zipWith_swap_prod_support' 📖	mathematical	—	Set Set.instLE setOf DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike Equiv.Perm.instMul Equiv.Perm.instOne Equiv.swap SetLike.coe Finset Finset.instSetLike SemilatticeSup.toMax Lattice.toSemilatticeSup Finset.instLattice toFinset	—	Finset.coe_union coe_toFinset mem_or_mem_of_zipWith_swap_prod_ne

---

← Back to Index