Concrete

📁 Source: Mathlib/GroupTheory/Perm/Cycle/Concrete.lean

Statistics

Metric	Count
Definitions formPerm, instRepr, isoCycle, isoCycle', toCycle, toList, «termC[_,]»	7
Theorems formPerm_apply_mem_eq_next, formPerm_coe, formPerm_eq_formPerm_iff, formPerm_eq_self_of_notMem, formPerm_reverse, formPerm_subsingleton, isCycle_formPerm, support_formPerm, existsUnique_cycle, existsUnique_cycle_nontrivial_subtype, existsUnique_cycle_subtype, toList_isRotated, exists_toCycle_toList, formPerm_toList, getElem_toList, length_toList, length_toList_pos_of_mem_support, mem_toCycle_iff_support, mem_toList_iff, next_toList_eq_apply, nodup_toCycle, nodup_toList, nontrivial_toCycle, pow_apply_mem_toList_iff_mem_support, toCycle_eq_toList, toCycle_next, toList_eq_nil_iff, toList_formPerm_isRotated_self, toList_formPerm_nil, toList_formPerm_nontrivial, toList_formPerm_singleton, toList_getElem_zero, toList_ne_singleton, toList_one, toList_pow_apply_eq_rotate, two_le_length_toList_iff_mem_support, cycleOf_formPerm, cycleType_formPerm, formPerm_apply_mem_eq_next, formPerm_disjoint_iff, isCycle_formPerm, pairwise_sameCycle_formPerm	42
Total	49

Cycle

Definitions

Name	Category	Theorems
formPerm 📖	CompOp	12 math math: formPerm_subsingleton, formPerm_coe, support_formPerm, CartanMatrix.D_three', Equiv.Perm.IsCycle.existsUnique_cycle_nontrivial_subtype, Equiv.Perm.IsCycle.existsUnique_cycle_subtype, formPerm_eq_formPerm_iff, isCycle_formPerm, formPerm_apply_mem_eq_next, formPerm_reverse, Equiv.Perm.IsCycle.existsUnique_cycle, formPerm_eq_self_of_notMem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
formPerm_apply_mem_eq_next 📖	mathematical	Nodup Cycle instMembership	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike formPerm next	—	List.formPerm_apply_mem_eq_next
formPerm_coe 📖	mathematical	—	formPerm ofList List.formPerm	—	—
formPerm_eq_formPerm_iff 📖	mathematical	Nodup	formPerm Subsingleton	—	length_subsingleton_iff Quotient.inductionOn₂' List.formPerm_eq_formPerm_iff
formPerm_eq_self_of_notMem 📖	mathematical	Nodup Cycle instMembership	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike formPerm	—	List.formPerm_apply_of_notMem
formPerm_reverse 📖	mathematical	Nodup	formPerm reverse nodup_reverse_iff Equiv.Perm Equiv.Perm.instInv	—	nodup_reverse_iff List.formPerm_reverse
formPerm_subsingleton 📖	mathematical	Subsingleton	formPerm Subsingleton.nodup Equiv.Perm Equiv.Perm.instOne	—	Subsingleton.nodup 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
isCycle_formPerm 📖	mathematical	Nodup Nontrivial	Equiv.Perm.IsCycle formPerm	—	List.isCycle_formPerm length_nontrivial
support_formPerm 📖	mathematical	Nodup Nontrivial	Equiv.Perm.support formPerm toFinset	—	List.support_formPerm_of_nodup zero_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instZeroLEOneClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat length_nontrivial

Equiv.Perm

Definitions

Name	Category	Theorems
instRepr 📖	CompOp	—
isoCycle 📖	CompOp	—
isoCycle' 📖	CompOp	—
toCycle 📖	CompOp	5 math math: mem_toCycle_iff_support, toCycle_eq_toList, nodup_toCycle, nontrivial_toCycle, exists_toCycle_toList
toList 📖	CompOp	18 math math: toList_formPerm_singleton, mem_toList_iff, length_toList_pos_of_mem_support, toList_eq_nil_iff, toList_formPerm_isRotated_self, formPerm_toList, SameCycle.toList_isRotated, toList_pow_apply_eq_rotate, toList_formPerm_nontrivial, toCycle_eq_toList, toList_formPerm_nil, toList_one, pow_apply_mem_toList_iff_mem_support, length_toList, two_le_length_toList_iff_mem_support, toList_getElem_zero, exists_toCycle_toList, nodup_toList
«termC[_,]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_toCycle_toList 📖	mathematical	IsCycle	toCycle Cycle.ofList toList	—	toCycle_eq_toList
formPerm_toList 📖	mathematical	—	List.formPerm toList cycleOf instDecidableRelSameCycle	—	cycleOf_eq_one_iff toList_eq_nil_iff notMem_support List.formPerm_nil ext SameCycle.exists_pow_eq_of_mem_support mem_support cycleOf_apply_apply_pow_self mem_toList_iff List.formPerm_apply_mem_eq_next nodup_toList next_toList_eq_apply pow_succ' mul_apply cycleOf_apply_of_not_sameCycle List.formPerm_apply_of_notMem
getElem_toList 📖	mathematical	toList	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike instPowNat	—	List.getElem_iterate
length_toList 📖	mathematical	—	toList Finset.card support cycleOf instDecidableRelSameCycle	—	List.length_iterate
length_toList_pos_of_mem_support 📖	mathematical	Finset Finset.instMembership support	toList	—	LT.lt.trans_le Nat.instAtLeastTwoHAddOfNat zero_lt_two Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid two_le_length_toList_iff_mem_support
mem_toCycle_iff_support 📖	mathematical	IsCycle	Cycle Cycle.instMembership toCycle	—	exists_toCycle_toList mem_toList_iff isCycle_iff_sameCycle mem_support toCycle_eq_toList pow_zero
mem_toList_iff 📖	mathematical	—	toList SameCycle Finset Finset.instMembership support	—	Mathlib.Tactic.Contrapose.contrapose₁ support_cycleOf_eq_nil_iff Nat.instCanonicallyOrderedAdd SameCycle.exists_pow_eq_of_mem_support
next_toList_eq_apply 📖	mathematical	toList	List.next DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	—	SameCycle.exists_pow_eq_of_mem_support mem_toList_iff length_toList getElem_toList List.next.congr_simp LE.le.trans_lt List.next_getElem nodup_toList mul_apply pow_succ' pow_mod_orderOf_cycleOf_apply IsCycle.orderOf isCycle_cycleOf mem_support
nodup_toCycle 📖	mathematical	IsCycle	Cycle.Nodup toCycle	—	toCycle_eq_toList nodup_toList
nodup_toList 📖	mathematical	—	toList	—	toList_eq_nil_iff notMem_support isCycle_cycleOf List.nodup_iff_injective_getElem getElem_toList cycleOf_pow_apply_self pow_zero mem_support IsCycle.support_pow_of_pos_of_lt_orderOf cycleOf_apply_self IsCycle.orderOf length_toList pow_inj_mod support_congr IsCycle.support_pow_eq_iff subset_refl Finset.instReflSubset IsCycle.exists_pow_eq Finite.of_fintype mul_apply Commute.eq Commute.pow_pow_self
nontrivial_toCycle 📖	mathematical	IsCycle	Cycle.Nontrivial toCycle	—	toCycle_eq_toList Cycle.nontrivial_coe_nodup_iff nodup_toList length_toList
pow_apply_mem_toList_iff_mem_support 📖	mathematical	—	toList DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike instPowNat Finset Finset.instMembership support	—	mem_toList_iff SameCycle.symm sameCycle_pow_left SameCycle.refl
toCycle_eq_toList 📖	mathematical	IsCycle	toCycle Cycle.ofList toList	—	Multiset.cons_erase toCycle.eq_1 Multiset.recOn_cons
toCycle_next 📖	mathematical	IsCycle Cycle Cycle.instMembership toCycle	Cycle.next nodup_toCycle DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike	—	nodup_toCycle exists_toCycle_toList Cycle.next.congr_simp next_toList_eq_apply
toList_eq_nil_iff 📖	mathematical	—	toList Finset Finset.instMembership support	—	—
toList_formPerm_isRotated_self 📖	mathematical	—	List.IsRotated toList List.formPerm	—	List.formPerm_eq_of_isRotated LT.lt.trans_eq LE.le.trans_lt List.length_rotate List.get_eq_get_rotate tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub le_of_lt LT.lt.trans_le Nat.instAtLeastTwoHAddOfNat zero_lt_two Nat.instZeroLEOneClass toList_formPerm_nontrivial
toList_formPerm_nil 📖	mathematical	—	toList List.formPerm	—	toList_one
toList_formPerm_nontrivial 📖	mathematical	—	toList List.formPerm LT.lt.trans_le PartialOrder.toPreorder Nat.instPartialOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid Nat.instAddMonoidWithOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Nat.instAtLeastTwoHAddOfNat zero_lt_two Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instAddCommMonoid Nat.instIsOrderedAddMonoid	—	List.isCycle_formPerm List.support_formPerm_of_nodup zero_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instZeroLEOneClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat LT.lt.trans_le zero_lt_two toList.eq_1 IsCycle.cycleOf_eq mem_support List.card_toFinset List.dedup_eq_self List.length_iterate LE.le.trans_lt List.getElem_iterate List.formPerm_pow_apply_getElem
toList_formPerm_singleton 📖	mathematical	—	toList List.formPerm	—	toList_one
toList_getElem_zero 📖	mathematical	Finset Finset.instMembership support	toList length_toList_pos_of_mem_support	—	length_toList_pos_of_mem_support List.getElem_iterate
toList_ne_singleton 📖	—	—	—	—	length_toList zero_add
toList_one 📖	mathematical	—	toList Equiv.Perm instOne	—	cycleOf_one support_one
toList_pow_apply_eq_rotate 📖	mathematical	—	toList DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike instPowNat	—	length_toList cycleOf_self_apply_pow List.length_rotate getElem_toList LE.le.trans_lt List.getElem_rotate pow_mod_card_support_cycleOf_self_apply pow_add mul_apply
two_le_length_toList_iff_mem_support 📖	mathematical	—	toList Finset Finset.instMembership support	—	length_toList

Equiv.Perm.IsCycle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
existsUnique_cycle 📖	mathematical	Equiv.Perm.IsCycle	ExistsUnique Cycle Cycle.Nodup Equiv.Perm Cycle.formPerm	—	nonempty_fintype Equiv.Perm.nodup_toList Equiv.Perm.formPerm_toList cycleOf_eq List.IsRotated.symm Equiv.Perm.toList_formPerm_isRotated_self Mathlib.Tactic.Contrapose.contrapose₂ List.formPerm_eq_one_iff List.mem_toFinset List.support_formPerm_le
existsUnique_cycle_nontrivial_subtype 📖	mathematical	Equiv.Perm.IsCycle	ExistsUnique Cycle Cycle.Nodup Cycle.Nontrivial Equiv.Perm Cycle.formPerm Subtype.prop	—	Subtype.prop existsUnique_cycle_subtype Cycle.Nodup.nontrivial_iff ne_one Cycle.formPerm_subsingleton
existsUnique_cycle_subtype 📖	mathematical	Equiv.Perm.IsCycle	ExistsUnique Cycle Cycle.Nodup Equiv.Perm Cycle.formPerm Subtype.prop	—	Subtype.prop existsUnique_cycle

Equiv.Perm.SameCycle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toList_isRotated 📖	mathematical	Equiv.Perm.SameCycle	List.IsRotated Equiv.Perm.toList	—	exists_pow_eq_of_mem_support pow_zero Equiv.Perm.toList_pow_apply_eq_rotate Equiv.Perm.toList_eq_nil_iff List.isRotated_nil_iff' mem_support_iff

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cycleOf_formPerm 📖	mathematical	—	Equiv.Perm.cycleOf formPerm Equiv.Perm.instDecidableRelSameCycle Subtype.fintype	—	nodup_attach Equiv.Perm.IsCycle.cycleOf_eq isCycle_formPerm formPerm_apply_mem_ne_self_iff
cycleType_formPerm 📖	mathematical	—	Equiv.Perm.cycleType Subtype.fintype formPerm Multiset Multiset.instSingleton	—	Equiv.Perm.cycleType_eq mul_one isCycle_formPerm nodup_attach instIsEmptyFalse support_formPerm_of_nodup zero_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instZeroLEOneClass Nat.instCharZero Nat.instAtLeastTwoHAddOfNat card_toFinset dedup_eq_self
formPerm_apply_mem_eq_next 📖	mathematical	—	DFunLike.coe Equiv.Perm EquivLike.toFunLike Equiv.instEquivLike formPerm next	—	LE.le.trans_lt next_getElem formPerm_apply_getElem
formPerm_disjoint_iff 📖	mathematical	—	Equiv.Perm.Disjoint formPerm	—	Equiv.Perm.disjoint_iff_eq_or_eq formPerm_apply_mem_eq_self_iff formPerm_apply_of_notMem
isCycle_formPerm 📖	mathematical	—	Equiv.Perm.IsCycle formPerm	—	Nat.instCanonicallyOrderedAdd Mathlib.Meta.NormNum.isNat_eq_false Nat.instCharZero Mathlib.Meta.NormNum.isNat_ofNat zero_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instZeroLEOneClass Nat.instAtLeastTwoHAddOfNat formPerm_apply_mem_ne_self_iff mem_of_formPerm_apply_ne zpow_natCast formPerm_pow_apply_head
pairwise_sameCycle_formPerm 📖	mathematical	—	Equiv.Perm.SameCycle formPerm	—	Equiv.Perm.IsCycle.sameCycle isCycle_formPerm formPerm_apply_mem_ne_self_iff

---

← Back to Index