Documentation Verification Report

Rotate

📁 Source: Mathlib/Logic/Equiv/Fin/Rotate.lean

Statistics

Metric	Count
Definitions `finCycle`, `finRotate`	2
Theorems `snoc_eq_cons_rotate`, `coe_finRotate`, `coe_finRotate_of_ne_last`, `coe_finRotate_symm_of_ne_zero`, `finCycle_apply`, `finCycle_eq_finRotate_iterate`, `finCycle_symm_apply`, `finRotate_apply_zero`, `finRotate_last`, `finRotate_last'`, `finRotate_of_lt`, `finRotate_one`, `finRotate_succ`, `finRotate_succ_apply`, `finRotate_succ_symm_apply`, `finRotate_symm_lt_iff_ne_zero`, `finRotate_zero`, `lt_finRotate_iff_ne_last`, `lt_finRotate_iff_ne_neg_one`	19
Total	21

Fin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`snoc_eq_cons_rotate` 📖	mathematical	—	`snoc` `cons` `DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `finRotate`	—	`LT.lt.trans_le` `finRotate_of_lt` `snoc.eq_1` `cons.eq_1` `finRotate_last'` `lt_irrefl`

(root)

Definitions

Name	Category	Theorems
`finCycle` 📖	CompOp	3 math math: `finCycle_eq_finRotate_iterate`, `finCycle_symm_apply`, `finCycle_apply`
`finRotate` 📖	CompOp	28 math math: `finRotate_succ_eq_decomposeFin`, `alternatingGroup.normalClosure_finRotate_five`, `lt_finRotate_iff_ne_last`, `finCycle_eq_finRotate_iterate`, `finRotate_of_lt`, `finRotate_apply_zero`, `finRotate_zero`, `Fin.snoc_eq_cons_rotate`, `finRotate_one`, `coe_finRotate`, `Equiv.Perm.finRotate_bit1_mem_alternatingGroup`, `finRotate_succ`, `coe_finRotate_symm_of_ne_zero`, `support_finRotate`, `coe_finRotate_of_ne_last`, `finRotate_succ_symm_apply`, `cycleType_finRotate`, `support_finRotate_of_le`, `Fin.cycleRange_last`, `cycleType_finRotate_of_le`, `finRotate_last'`, `sign_finRotate`, `finRotate_symm_lt_iff_ne_zero`, `finRotate_last`, `isCycle_finRotate_of_le`, `finRotate_succ_apply`, `lt_finRotate_iff_ne_neg_one`, `isCycle_finRotate`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_finRotate` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `finRotate`	—	`finRotate_succ_apply`
`coe_finRotate_of_ne_last` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `finRotate`	—	`finRotate_succ_apply`
`coe_finRotate_symm_of_ne_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finRotate`	—	`finRotate_succ_symm_apply` `Fin.neZero` `Fin.val_sub_one_of_ne_zero`
`finCycle_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `finCycle`	—	—
`finCycle_eq_finRotate_iterate` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `finCycle` `Nat.iterate` `finRotate`	—	`add_zero` `Function.iterate_succ'` `Fin.val_eq_val` `finRotate_succ_apply` `finCycle_apply` `add_assoc`
`finCycle_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finCycle`	—	—
`finRotate_apply_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `finRotate`	—	`finRotate_succ_apply` `zero_add`
`finRotate_last` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `finRotate`	—	`finRotate_last'`
`finRotate_last'` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `finRotate`	—	`le_rfl` `finAddFlip_apply_mk_right`
`finRotate_of_lt` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `finRotate` `LT.lt.trans_le` `Nat.instPreorder`	—	`LT.lt.trans_le` `finAddFlip_apply_mk_left`
`finRotate_one` 📖	mathematical	—	`finRotate` `Equiv.refl`	—	`Equiv.equiv_subsingleton_dom`
`finRotate_succ` 📖	mathematical	—	`finRotate` `Equiv.trans` `finAddFlip` `finCongr`	—	—
`finRotate_succ_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `finRotate`	—	`finRotate_last` `finRotate_of_lt`
`finRotate_succ_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finRotate`	—	`Equiv.symm_apply_eq` `finRotate_succ_apply` `sub_add_cancel`
`finRotate_symm_lt_iff_ne_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `finRotate`	—	`coe_finRotate_symm_of_ne_zero`
`finRotate_zero` 📖	mathematical	—	`finRotate` `Equiv.refl`	—	—
`lt_finRotate_iff_ne_last` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `finRotate`	—	`finRotate_succ_apply` `Fin.lt_last_iff_ne_last`
`lt_finRotate_iff_ne_neg_one` 📖	mathematical	—	`DFunLike.coe` `Equiv.Perm` `EquivLike.toFunLike` `Equiv.instEquivLike` `finRotate`	—	`lt_finRotate_iff_ne_last` `not_iff_not` `Fin.neg_last` `neg_neg`

---

← Back to Index