product_right — Mathlib

English

If l1 ~ l2, then for any t1, the product l1 t1 is permutation-equivalent to the product l2 t1.

Русский

Если l1 перестановочно эквивалентен l2, то произведение l1 с t1 перестановочно эквивалентно произведению l2 с t1.

LaTeX

$$$l_1 \\sim l_2 \\Rightarrow (l_1 \\mathrm{.product} \\; t_1) \\sim (l_2 \\mathrm{.product} \\; t_1)$$$

Lean4

theorem product_right {l₁ l₂ : List α} (t₁ : List β) (p : l₁ ~ l₂) : product l₁ t₁ ~ product l₂ t₁ :=
  p.flatMap_right _

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