instIsSymmOpZipWith — Mathlib

English

If f is symmetric (IsSymmOp f), then zipWith f is a symmetric binary operation on lists.

Русский

Если f симметрична, то zipWith f является симметричной бинарной операцией над списками.

LaTeX

$$$[IsSymmOp f] \Rightarrow IsSymmOp (zipWith f)$, i.e., zipWith f la lb = zipWith f lb la for all la,lb.$$

Lean4

instance (f : α → α → β) [IsSymmOp f] : IsSymmOp (zipWith f) :=
  ⟨fun _ _ => zipWith_comm_of_comm IsSymmOp.symm_op⟩

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