Fin

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

Statistics

Metric	Count
Definitions `decomposeFin`, `cycleIcc`, `cycleRange`	3
Theorems `symm_sign`, `decomposeFin_symm_apply_one`, `decomposeFin_symm_apply_succ`, `decomposeFin_symm_apply_zero`, `decomposeFin_symm_of_one`, `decomposeFin_symm_of_refl`, `prod_Iio_comp_eq_sign_mul_prod`, `prod_Ioi_comp_eq_sign_mul_prod`, `sign_eq_prod_prod_Iio`, `sign_eq_prod_prod_Ioi`, `coe_cycleRange_of_le`, `coe_cycleRange_of_lt`, `cons_apply_cycleRange`, `cons_comp_cycleRange`, `trans`, `trans_left_one`, `trans_right_one`, `cycleIcc_def_gt`, `cycleIcc_def_gt'`, `cycleIcc_def_le`, `cycleIcc_eq`, `cycleIcc_ge`, `cycleIcc_of_ge_of_lt`, `cycleIcc_of_gt`, `cycleIcc_of_last`, `cycleIcc_of_le_of_le`, `cycleIcc_of_lt`, `cycleIcc_to_cycleRange`, `cycleIcc_zero_eq_cycleRange`, `cycleRange_apply`, `cycleRange_last`, `cycleRange_mk_zero`, `cycleRange_of_eq`, `cycleRange_of_gt`, `cycleRange_of_le`, `cycleRange_of_lt`, `cycleRange_self`, `cycleRange_succAbove`, `cycleRange_symm_succ`, `cycleRange_symm_zero`, `cycleRange_zero`, `cycleType_cycleIcc_of_ge`, `cycleType_cycleIcc_of_lt`, `cycleType_cycleRange`, `insertNth_apply_cycleRange_symm`, `insertNth_comp_cycleRange_symm`, `instNeZeroNatHSubVal_mathlib`, `isCycle_cycleIcc`, `isCycle_cycleRange`, `isThreeCycle_cycleRange_two`, `sign_cycleIcc_of_eq`, `sign_cycleIcc_of_ge`, `sign_cycleIcc_of_le`, `sign_cycleRange`, `succAbove_cycleRange`, `univ_perm_fin_succ`, `cycleType_finRotate`, `cycleType_finRotate_of_le`, `finRotate_succ_eq_decomposeFin`, `isCycle_finRotate`, `isCycle_finRotate_of_le`, `sign_finRotate`, `support_finRotate`, `support_finRotate_of_le`	64
Total	67

Equiv.Perm

Definitions

Name	Category	Theorems
`decomposeFin` 📖	CompOp	8 math math: `decomposeFin_symm_of_refl`, `decomposeFin_symm_apply_one`, `decomposeFin.symm_sign`, `finRotate_succ_eq_decomposeFin`, `decomposeFin_symm_apply_succ`, `Finset.univ_perm_fin_succ`, `decomposeFin_symm_of_one`, `decomposeFin_symm_apply_zero`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`decomposeFin_symm_apply_one` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv` `Equiv.symm` `decomposeFin` `Equiv.swap`	—	`decomposeFin_symm_apply_succ`
`decomposeFin_symm_apply_succ` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv` `Equiv.symm` `decomposeFin` `Equiv.swap`	—	`Equiv.swap_self` `finSuccEquiv_succ` `finSuccEquiv_symm_some` `Equiv.permCongr_mul` `Equiv.swap_apply_right` `finSuccEquiv_symm_none`
`decomposeFin_symm_apply_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv` `Equiv.symm` `decomposeFin`	—	`Equiv.permCongr_mul` `finSuccEquiv_symm_none` `Equiv.swap_apply_left` `Equiv.symm_apply_apply`
`decomposeFin_symm_of_one` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `decomposeFin` `instOne` `Equiv.swap`	—	`decomposeFin_symm_of_refl`
`decomposeFin_symm_of_refl` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `decomposeFin` `Equiv.refl` `Equiv.swap`	—	`Equiv.optionCongr_refl` `mul_refl` `Equiv.trans_swap_trans_symm` `finSuccEquiv_symm_none` `Equiv.symm_apply_apply`
`prod_Iio_comp_eq_sign_mul_prod` 📖	mathematical	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	`Finset.prod` `CommRing.toCommMonoid` `Finset.univ` `Fin.fintype` `Finset.Iio` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Fin.instLocallyFiniteOrderBot` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `Units.val` `Int.instMonoid` `MonoidHom` `Units` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `permGroup` `Units.instMulOneClass` `MonoidHom.instFunLike` `sign`	—	`sign_inv` `sign_eq_prod_prod_Iio` `Finset.prod_sigma'` `Units.coe_prod` `Int.cast_prod` `Finset.ext` `LE.le.lt_of_ne` `inf_le_sup` `EquivLike.toEmbeddingLike` `LT.lt.ne` `lt_or_ge` `Equiv.apply_symm_apply` `sup_of_le_right` `LT.lt.le` `inf_of_le_left` `sup_of_le_left` `inf_of_le_right` `Finset.prod_image` `Finset.injOn_of_card_image_eq` `Finset.prod_congr` `inf_eq_left` `Equiv.symm_apply_apply` `sup_eq_right` `LT.lt.not_gt` `Int.cast_neg` `Int.cast_one` `neg_mul` `one_mul` `inf_eq_right` `sup_eq_left`
`prod_Ioi_comp_eq_sign_mul_prod` 📖	mathematical	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing`	`Finset.prod` `CommRing.toCommMonoid` `Finset.univ` `Fin.fintype` `Finset.Ioi` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Fin.instLocallyFiniteOrderTop` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `Units.val` `Int.instMonoid` `MonoidHom` `Units` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `permGroup` `Units.instMulOneClass` `MonoidHom.instFunLike` `sign`	—	`Finset.prod_comm'` `prod_Iio_comp_eq_sign_mul_prod`
`sign_eq_prod_prod_Iio` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Equiv.Perm` `Units` `Int.instMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `permGroup` `Units.instMulOneClass` `MonoidHom.instFunLike` `sign` `Fin.fintype` `Finset.prod` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `Int.instCommMonoid` `Finset.univ` `Finset.Iio` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Fin.instLocallyFiniteOrderBot` `EquivLike.toFunLike` `Equiv.instEquivLike` `Units.instOne` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing`	—	`swap_induction_on` `Finite.of_fintype` `sign_one` `signAux_one` `signAux_mul` `sign_mul` `sign_swap` `signAux_swap` `Finset.prod_sigma'` `signAux.eq_1` `Finset.prod_congr`
`sign_eq_prod_prod_Ioi` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `Equiv.Perm` `Units` `Int.instMonoid` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `permGroup` `Units.instMulOneClass` `MonoidHom.instFunLike` `sign` `Fin.fintype` `Finset.prod` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `Int.instCommMonoid` `Finset.univ` `Finset.Ioi` `PartialOrder.toPreorder` `Fin.instPartialOrder` `Fin.instLocallyFiniteOrderTop` `EquivLike.toFunLike` `Equiv.instEquivLike` `Units.instOne` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing`	—	`sign_eq_prod_prod_Iio` `Finset.prod_comm'`

Equiv.Perm.decomposeFin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`symm_sign` 📖	mathematical	—	`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` `Fin.fintype` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Equiv.Perm.decomposeFin` `Units.instMul` `Units.instOne` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing`	—	`Equiv.swap_self` `Equiv.Perm.sign_permCongr` `Equiv.optionCongr_sign` `one_mul` `finSuccEquiv_succ` `Equiv.permCongr_mul` `Equiv.Perm.sign_mul` `Equiv.Perm.sign_swap'` `neg_mul`

Fin

Definitions

Name	Category	Theorems
`cycleIcc` 📖	CompOp	21 math math: `sign_cycleIcc_of_eq`, `cycleIcc_ge`, `cycleIcc.trans_right_one`, `cycleIcc_of_last`, `cycleIcc_of_gt`, `cycleType_cycleIcc_of_ge`, `cycleIcc.trans_left_one`, `sign_cycleIcc_of_ge`, `cycleIcc_to_cycleRange`, `sign_cycleIcc_of_le`, `cycleIcc_of_ge_of_lt`, `cycleIcc_def_gt`, `cycleIcc_zero_eq_cycleRange`, `cycleIcc_eq`, `cycleIcc_of_lt`, `cycleType_cycleIcc_of_lt`, `cycleIcc_def_le`, `isCycle_cycleIcc`, `cycleIcc_of_le_of_le`, `cycleIcc_def_gt'`, `cycleIcc.trans`
`cycleRange` 📖	CompOp	26 math math: `cycleRange_succAbove`, `cycleRange_apply`, `sign_cycleRange`, `coe_cycleRange_of_lt`, `cycleRange_zero`, `coe_cycleRange_of_le`, `cycleIcc_to_cycleRange`, `cons_apply_cycleRange`, `cycleRange_symm_zero`, `cycleRange_of_eq`, `succAbove_cycleRange`, `cycleRange_of_le`, `isCycle_cycleRange`, `cycleIcc_zero_eq_cycleRange`, `cycleRange_of_lt`, `cycleRange_symm_succ`, `cycleRange_mk_zero`, `insertNth_comp_cycleRange_symm`, `isThreeCycle_cycleRange_two`, `cycleRange_last`, `cycleRange_of_gt`, `cycleIcc_def_le`, `cycleType_cycleRange`, `cons_comp_cycleRange`, `insertNth_apply_cycleRange_symm`, `cycleRange_self`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_cycleRange_of_le` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleRange`	—	`le_rfl` `LT.lt.not_ge` `cycleRange_of_le` `lt_of_le_of_ne`
`coe_cycleRange_of_lt` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleRange`	—	`coe_cycleRange_of_le` `LT.lt.le` `LT.lt.ne`
`cons_apply_cycleRange` 📖	mathematical	—	`cons` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleRange` `insertNth`	—	`insertNth_apply_cycleRange_symm` `Equiv.symm_apply_apply`
`cons_comp_cycleRange` 📖	mathematical	—	`cons` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleRange` `insertNth`	—	`cons_apply_cycleRange`
`cycleIcc_def_gt` 📖	mathematical	—	`cycleIcc` `Equiv.Perm` `Equiv.Perm.instOne`	—	`sub_val_lt_sub`
`cycleIcc_def_gt'` 📖	mathematical	—	`cycleIcc` `Equiv.Perm` `Equiv.Perm.instOne`	—	`sub_val_lt_sub`
`cycleIcc_def_le` 📖	mathematical	—	`cycleIcc` `Equiv.Perm.extendDomain` `cycleRange` `sub_val_lt_sub` `Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `natAdd_castLEEmb` `Fintype.decidableMemRangeFintype` `fintype` `Function.Embedding.toEquivRange`	—	`sub_val_lt_sub`
`cycleIcc_eq` 📖	mathematical	—	`cycleIcc` `Equiv.Perm` `Equiv.Perm.instOne`	—	`Equiv.Perm.ext` `lt_trichotomy` `cycleIcc_of_lt` `cycleIcc_of_le_of_le` `cycleIcc_of_gt`
`cycleIcc_ge` 📖	mathematical	—	`cycleIcc` `Equiv.Perm` `Equiv.Perm.instOne`	—	`cycleIcc_def_gt` `cycleIcc_eq`
`cycleIcc_of_ge_of_lt` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleIcc`	—	`cycleIcc_of_le_of_le` `le_of_lt`
`cycleIcc_of_gt` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleIcc`	—	`range_natAdd_castLEEmb` `Nat.instOrderedSub` `Set.mem_range_self` `sub_val_lt_sub` `cycleIcc_to_cycleRange` `cycleRange_of_gt` `cycleIcc_def_gt'`
`cycleIcc_of_last` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleIcc`	—	`cycleIcc_of_le_of_le` `ge_of_eq`
`cycleIcc_of_le_of_le` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleIcc`	—	`le_trans` `range_natAdd_castLEEmb` `Nat.instOrderedSub` `Set.mem_range_self` `sub_val_lt_sub` `cycleIcc_to_cycleRange` `instNeZeroNatHSubVal_mathlib` `cycleRange_of_eq` `zero_add` `cycleRange_of_lt` `subNat.eq_1`
`cycleIcc_of_lt` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleIcc`	—	`sub_val_lt_sub` `cycleIcc_def_le` `Equiv.Perm.extendDomain_apply_not_subtype` `range_natAdd_castLEEmb` `Nat.instOrderedSub` `cycleIcc_def_gt'`
`cycleIcc_to_cycleRange` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `DFunLike.coe` `Function.Embedding` `Function.instFunLikeEmbedding` `natAdd_castLEEmb`	`Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleIcc` `cycleRange` `sub_val_lt_sub` `Equiv` `Set.Elem` `Equiv.symm` `Function.Embedding.toEquivRange` `fintype`	—	`sub_val_lt_sub` `cycleIcc_def_le` `Equiv.Perm.extendDomain_apply_subtype`
`cycleIcc_zero_eq_cycleRange` 📖	mathematical	—	`cycleIcc` `cycleRange`	—	`Equiv.Perm.ext` `lt_trichotomy` `cycleIcc_of_ge_of_lt` `cycleRange_of_lt` `cycleIcc_of_le_of_le` `cycleRange_self` `cycleIcc_of_gt` `cycleRange_of_gt`
`cycleRange_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleRange`	—	`cycleRange_of_lt` `cycleRange_of_eq` `cycleRange_of_gt` `lt_of_le_of_ne` `le_of_not_gt`
`cycleRange_last` 📖	mathematical	—	`cycleRange` `finRotate`	—	`Equiv.Perm.ext` `coe_cycleRange_of_le` `coe_finRotate`
`cycleRange_mk_zero` 📖	mathematical	—	`cycleRange` `Equiv.Perm` `Equiv.Perm.instOne`	—	`NeZero.of_pos` `cycleRange_zero`
`cycleRange_of_eq` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleRange`	—	`cycleRange_of_le` `Eq.le`
`cycleRange_of_gt` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleRange`	—	`cycleRange.eq_1` `Equiv.Perm.extendDomain_apply_not_subtype` `range_castLE` `Nat.instNoMaxOrder`
`cycleRange_of_le` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleRange`	—	`range_castLE` `Nat.instNoMaxOrder` `cycleRange.eq_1` `Equiv.Perm.extendDomain_apply_subtype` `Set.mem_range_self` `Function.Embedding.toEquivRange_apply` `Equiv.symm_apply_apply` `finRotate_last` `val_add_one_of_lt'` `finRotate_succ_apply`
`cycleRange_of_lt` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleRange`	—	`cycleRange_of_le` `LT.lt.le` `LT.lt.ne`
`cycleRange_self` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleRange`	—	`cycleRange_of_eq`
`cycleRange_succAbove` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleRange` `succAbove`	—	`lt_or_ge` `succAbove_of_castSucc_lt` `cycleRange_of_lt` `succAbove_of_le_castSucc` `cycleRange_of_gt`
`cycleRange_symm_succ` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `cycleRange` `succAbove`	—	`Equiv.injective` `Equiv.apply_symm_apply` `cycleRange_succAbove`
`cycleRange_symm_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `cycleRange`	—	`Equiv.injective` `Equiv.apply_symm_apply` `cycleRange_self`
`cycleRange_zero` 📖	mathematical	—	`cycleRange` `Equiv.Perm` `Equiv.Perm.instOne`	—	`Equiv.Perm.ext` `LE.le.eq_or_lt` `cycleRange_self` `cycleRange_of_gt` `Equiv.Perm.one_apply`
`cycleType_cycleIcc_of_ge` 📖	mathematical	—	`Equiv.Perm.cycleType` `fintype` `cycleIcc` `Multiset` `Multiset.instEmptyCollection`	—	`cycleIcc_ge`
`cycleType_cycleIcc_of_lt` 📖	mathematical	—	`Equiv.Perm.cycleType` `fintype` `cycleIcc` `Multiset` `Multiset.instSingleton`	—	`sub_val_lt_sub` `le_of_lt` `Equiv.Perm.cycleType.congr_simp` `cycleIcc_def_le` `Equiv.Perm.cycleType_extendDomain` `cycleType_cycleRange` `castLT_sub_nezero`
`cycleType_cycleRange` 📖	mathematical	—	`Equiv.Perm.cycleType` `fintype` `cycleRange` `Multiset` `Multiset.instSingleton`	—	`Equiv.Perm.cycleType_extendDomain` `cycleType_finRotate`
`insertNth_apply_cycleRange_symm` 📖	mathematical	—	`insertNth` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `cycleRange` `cons`	—	`cycleRange_symm_zero` `insertNth_apply_same` `cons_zero` `cycleRange_symm_succ` `insertNth_apply_succAbove` `cons_succ`
`insertNth_comp_cycleRange_symm` 📖	mathematical	—	`insertNth` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `cycleRange` `cons`	—	`insertNth_apply_cycleRange_symm`
`instNeZeroNatHSubVal_mathlib` 📖	mathematical	—	`MulZeroClass.toZero` `Nat.instMulZeroClass`	—	`NeZero.of_pos`
`isCycle_cycleIcc` 📖	mathematical	—	`Equiv.Perm.IsCycle` `cycleIcc`	—	`sub_val_lt_sub` `le_of_lt` `cycleIcc_def_le` `Equiv.Perm.IsCycle.extendDomain` `isCycle_cycleRange` `castLT_sub_nezero`
`isCycle_cycleRange` 📖	mathematical	—	`Equiv.Perm.IsCycle` `cycleRange`	—	`Equiv.Perm.IsCycle.extendDomain` `isCycle_finRotate`
`isThreeCycle_cycleRange_two` 📖	mathematical	—	`Equiv.Perm.IsThreeCycle` `fintype` `cycleRange`	—	`Equiv.Perm.IsThreeCycle.eq_1` `cycleType_cycleRange` `two_ne_zero` `instNeZeroHAddNatOfNat_mathlib` `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` `Nat.instNoMaxOrder` `Nat.instCanonicallyOrderedAdd`
`sign_cycleIcc_of_eq` 📖	mathematical	—	`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` `fintype` `cycleIcc` `Units.instOne`	—	`sign_cycleIcc_of_le` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero`
`sign_cycleIcc_of_ge` 📖	mathematical	—	`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` `fintype` `cycleIcc` `Units.instOne`	—	`cycleIcc_def_gt'` `Equiv.Perm.sign_one` `sign_cycleIcc_of_eq`
`sign_cycleIcc_of_le` 📖	mathematical	—	`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` `fintype` `cycleIcc` `Monoid.toNatPow` `Units.instMonoid` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `Units.instOne`	—	`sub_val_lt_sub` `cycleIcc_def_le` `Equiv.Perm.sign_extendDomain` `sign_cycleRange`
`sign_cycleRange` 📖	mathematical	—	`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` `fintype` `cycleRange` `Monoid.toNatPow` `Units.instMonoid` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `Units.instOne`	—	`Equiv.Perm.sign_extendDomain` `sign_finRotate`
`succAbove_cycleRange` 📖	mathematical	—	`succAbove` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `cycleRange` `Equiv.swap`	—	`lt_trichotomy` `lt_of_lt_of_le` `cycleRange_of_lt` `succAbove_of_castSucc_lt` `Nat.instNoMaxOrder` `Equiv.swap_apply_of_ne_of_ne` `succ_injective` `LT.lt.ne` `cycleRange_self` `Equiv.swap_apply_right` `cycleRange_of_gt` `succAbove_of_le_castSucc`

Fin.cycleIcc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`trans` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Fin.cycleIcc`	—	`lt_or_ge` `Fin.cycleIcc_of_lt` `lt_of_lt_of_le` `Fin.cycleIcc_of_gt` `lt_of_le_of_lt` `Fin.cycleIcc_of_le_of_le` `le_of_lt` `Fin.cycleIcc_of_last` `Fin.lt_add_one_of_succ_lt`
`trans_left_one` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Fin.cycleIcc`	—	`Fin.cycleIcc_ge` `CompTriple.comp_eq` `CompTriple.instId_comp` `CompTriple.instIsIdId`
`trans_right_one` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Fin.cycleIcc`	—	`Fin.cycleIcc_ge` `CompTriple.comp_eq` `CompTriple.instComp_id` `CompTriple.instIsIdId`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`univ_perm_fin_succ` 📖	mathematical	—	`univ` `Equiv.Perm` `Equiv.instFintype` `Fin.fintype` `map` `Equiv.toEmbedding` `Equiv.symm` `Equiv.Perm.decomposeFin` `instFintypeProd`	—	`univ_map_equiv_to_embedding`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cycleType_finRotate` 📖	mathematical	—	`Equiv.Perm.cycleType` `Fin.fintype` `finRotate` `Multiset` `Multiset.instSingleton`	—	`Equiv.Perm.IsCycle.cycleType` `isCycle_finRotate` `support_finRotate` `Fintype.card.eq_1` `Fintype.card_fin`
`cycleType_finRotate_of_le` 📖	mathematical	—	`Equiv.Perm.cycleType` `Fin.fintype` `finRotate` `Multiset` `Multiset.instSingleton`	—	`ExistsAddOfLE.exists_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `add_comm` `cycleType_finRotate`
`finRotate_succ_eq_decomposeFin` 📖	mathematical	—	`finRotate` `DFunLike.coe` `Equiv` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `Equiv.Perm.decomposeFin`	—	`Equiv.Perm.ext` `finRotate_one` `Equiv.Perm.decomposeFin_symm_of_refl` `Equiv.swap_self` `finRotate_succ_apply` `zero_add` `Equiv.Perm.decomposeFin_symm_apply_zero` `coe_finRotate` `Equiv.Perm.decomposeFin_symm_apply_succ` `if_congr` `Equiv.swap_apply_right` `Function.Injective.map_swap` `Fin.val_injective` `Equiv.swap_apply_of_ne_of_ne`
`isCycle_finRotate` 📖	mathematical	—	`Equiv.Perm.IsCycle` `finRotate`	—	`finRotate_succ_apply` `zero_add` `Fin.instNeZeroHAddNatOfNat_mathlib` `zpow_natCast` `pow_succ'` `Equiv.Perm.mul_apply` `coe_finRotate_of_ne_last` `lt_trans` `ne_of_lt`
`isCycle_finRotate_of_le` 📖	mathematical	—	`Equiv.Perm.IsCycle` `finRotate`	—	`ExistsAddOfLE.exists_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `add_comm` `isCycle_finRotate`
`sign_finRotate` 📖	mathematical	—	`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` `Fin.fintype` `finRotate` `Monoid.toNatPow` `Units.instMonoid` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Int.instCommRing` `Units.instOne`	—	`finRotate_one` `Equiv.Perm.sign_refl` `pow_zero` `finRotate_succ_eq_decomposeFin` `Equiv.Perm.decomposeFin.symm_sign` `Fin.instNeZeroHAddNatOfNat_mathlib` `neg_mul` `one_mul` `pow_succ` `mul_neg` `mul_one`
`support_finRotate` 📖	mathematical	—	`Equiv.Perm.support` `Fin.fintype` `finRotate` `Finset.univ`	—	`Finset.ext` `finRotate_succ_apply` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Fin.instNeZeroHAddNatOfNat_mathlib`
`support_finRotate_of_le` 📖	mathematical	—	`Equiv.Perm.support` `Fin.fintype` `finRotate` `Finset.univ`	—	`ExistsAddOfLE.exists_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `add_comm` `support_finRotate`

---

← Back to Index