cycleIcc_eq — Mathlib

English

For every n > 0 and every i in Fin(n), the cycle from i to i is the identity permutation.

Русский

Для любого n > 0 и любого i ∈ Fin(n) цикл cycleIcc(i,i) тождествен по отношению к перестановке.

LaTeX

$$$\\forall {n : \\mathbb{N}} \\; \\forall {i : \\mathrm{Fin}(n)},\\; n > 0 \\Rightarrow \\mathrm{cycleIcc}(i,i) = 1$$$

Lean4

theorem cycleIcc_eq [NeZero n] : cycleIcc i i = 1 := by
  ext k
  simp only [Perm.coe_one, id_eq]
  rcases lt_trichotomy k i with ch | ch | ch
  · simp [-cycleIcc_def_le, cycleIcc_of_lt, ch]
  · simp [-cycleIcc_def_le, ch]
  · simp [-cycleIcc_def_le, cycleIcc_of_gt, ch]

Похожие утверждения