cycleType_formPerm — Mathlib

English

Equality of formPerms is equivalent to equality of cycles up to subsingleton structure.

Русский

Равенство formPerm эквивалентно равенству циклов с учётом подпоследовательной структуры.

LaTeX

$$$\\text{formPerm\_eq\_formPerm\_iff}(s,s') \\iff \\text{(s = s') ∨ (s.Subsingleton ∧ s'.Subsingleton)}$$$

Lean4

theorem cycleType_formPerm (hl : Nodup l) (hn : 2 ≤ l.length) : cycleType l.attach.formPerm = { l.length } :=
  by
  rw [← length_attach] at hn
  rw [← nodup_attach] at hl
  rw [cycleType_eq [l.attach.formPerm]]
  · simp only [map, Function.comp_apply]
    rw [support_formPerm_of_nodup _ hl, card_toFinset, dedup_eq_self.mpr hl]
    · simp
    · intro x h
      simp [h] at hn
  · simp
  · simpa using isCycle_formPerm hl hn
  · simp

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