permutations — Mathlib

English

For all s,t, permutations s is permutation-equivalent to permutations t if and only if s is permutation-equivalent to t.

Русский

Для любых s,t: permutations s ~ permutations t тогда и только тогда, когда s ~ t.

LaTeX

$$$$\operatorname{permutations} s ~ \operatorname{permutations} t \ \iff\ \ s ~ t $$$$

Lean4

theorem permutations {s t : List α} (h : s ~ t) : permutations s ~ permutations t :=
  (permutations_perm_permutations' _).trans <| h.permutations'.trans (permutations_perm_permutations' _).symm

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