isCycle_finRotate — Mathlib

English

For all n, finRotate(n+2) is a single cycle.

Русский

Для всех n перестановка finRotate(n+2) образует один цикл.

LaTeX

$$$ \\mathrm{IsCycle}(\\mathrm{finRotate}(n+2))$$$

Lean4

theorem isCycle_finRotate {n : ℕ} : IsCycle (finRotate (n + 2)) :=
  by
  refine ⟨0, by simp, fun x hx' => ⟨x, ?_⟩⟩
  clear hx'
  obtain ⟨x, hx⟩ := x
  rw [zpow_natCast, Fin.ext_iff, Fin.val_mk]
  induction x with
  | zero => rfl
  | succ x ih =>
    rw [pow_succ', Perm.mul_apply, coe_finRotate_of_ne_last, ih (lt_trans x.lt_succ_self hx)]
    rw [Ne, Fin.ext_iff, ih (lt_trans x.lt_succ_self hx), Fin.val_last]
    exact ne_of_lt (Nat.lt_of_succ_lt_succ hx)

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