isCycle_formPerm — Mathlib

English

If l is nodup and of length at least 2, then l.formPerm is a cycle.

Русский

Если список без повторов имеет длину не менее 2, то formPerm является циклом.

LaTeX

$$$IsCycle(l.formPerm)$$$

Lean4

theorem isCycle_formPerm (hl : Nodup l) (hn : 2 ≤ l.length) : IsCycle (formPerm l) :=
  by
  rcases l with - | ⟨x, l⟩
  · norm_num at hn
  induction l generalizing x with
  | nil => norm_num at hn
  | cons y l =>
    use x
    constructor
    · rwa [formPerm_apply_mem_ne_self_iff _ hl _ mem_cons_self]
    · intro w hw
      have : w ∈ x :: y :: l := mem_of_formPerm_apply_ne hw
      obtain ⟨k, hk, rfl⟩ := getElem_of_mem this
      use k
      simp only [zpow_natCast, formPerm_pow_apply_head _ _ hl k, Nat.mod_eq_of_lt hk]

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