formPerm — Mathlib

English

The formPerm of a reversed cycle equals the inverse of the formPerm.

Русский

FormPerm для перевёрнутого цикла равен обратному formPerm.

LaTeX

$$$\\text{formPerm\\_reverse}(s,h) = (\\text{formPerm } s h)^{-1}$$$

Lean4

/-- A cycle `s : Cycle α`, given `Nodup s` can be interpreted as an `Equiv.Perm α`
where each element in the list is permuted to the next one, defined as `formPerm`.
-/
def formPerm : ∀ s : Cycle α, Nodup s → Equiv.Perm α := fun s =>
  Quotient.hrecOn s (fun l _ => List.formPerm l) fun l₁ l₂ (h : l₁ ~r l₂) =>
    by
    apply Function.hfunext
    · ext
      exact h.nodup_iff
    · intro h₁ h₂ _
      exact heq_of_eq (formPerm_eq_of_isRotated h₁ h)

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