formPerm_pow_length_eq_one_of_nodup

English

If l is Nodup, then (formPerm l)^length l = 1.

Русский

Если l без повторов, то (formPerm l)^length l = 1.

LaTeX

$$$\forall {\alpha} [\DecidableEq \alpha],\ (l:\,\mathrm{List}\ \alpha),\ l.Nodup → (\mathrm{HPow}.hPow\ l.formPerm\ l.length) = 1$$$

Lean4

theorem formPerm_pow_length_eq_one_of_nodup (hl : Nodup l) : formPerm l ^ length l = 1 :=
  by
  ext x
  by_cases hx : x ∈ l
  · obtain ⟨k, hk, rfl⟩ := getElem_of_mem hx
    simp [formPerm_pow_apply_getElem _ hl, Nat.mod_eq_of_lt hk]
  · have : x ∉ {x | (l.formPerm ^ l.length) x ≠ x} := by
      intro H
      refine hx ?_
      replace H := set_support_zpow_subset l.formPerm l.length H
      simpa using support_formPerm_le' _ H
    simpa using this

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