product_left — Mathlib

English

If l is fixed and t1 ~ t2, then product l t1 ~ product l t2.

Русский

Если фиксирован список l, и t1 перестановочно эквивален t2, то l произв. t1 перестановочно эквивален l произв. t2.

LaTeX

$$$t_1 \\sim t_2 \\Rightarrow (l \\mathrm{.product} \\; t_1) \\sim (l \\mathrm{.product} \\; t_2)$$$

Lean4

theorem product_left (l : List α) {t₁ t₂ : List β} (p : t₁ ~ t₂) : product l t₁ ~ product l t₂ :=
  (Perm.flatMap_left _) fun _ _ => p.map _

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