English
For any list l with length at least 2 and nodup, the toList of formPerm l at its first element equals l.
Русский
Для любого списка l длины ≥ 2 и без повторов, toList formPerm l на первом элементе равен самому списку l.
LaTeX
$$$$\text{If } hl:\ge 2,\ hn:\mathrm{Nodup}(l),\ then\ toList(\mathrm{formPerm}\ l) (l.get ⟨0,\ _⟩) = l.$$$$
Lean4
theorem toList_formPerm_nontrivial (l : List α) (hl : 2 ≤ l.length) (hn : Nodup l) :
toList (formPerm l) (l.get ⟨0, (zero_lt_two.trans_le hl)⟩) = l :=
by
have hc : l.formPerm.IsCycle := List.isCycle_formPerm hn hl
have hs : l.formPerm.support = l.toFinset :=
by
refine support_formPerm_of_nodup _ hn ?_
rintro _ rfl
simp at hl
rw [toList, hc.cycleOf_eq (mem_support.mp _), hs, card_toFinset, dedup_eq_self.mpr hn]
· refine ext_getElem (by simp) fun k hk hk' => ?_
simp only [get_eq_getElem, getElem_iterate, iterate_eq_pow, formPerm_pow_apply_getElem _ hn, zero_add,
Nat.mod_eq_of_lt hk']
· simp [hs]
