noncommFold — Mathlib

English

If op is associative and commutative, then noncommFold op s comm a = fold op a s.

Русский

Если операция ассоциативна и коммутативна, то noncommFold op s comm a = fold op a s.

LaTeX

$$$\\mathrm{noncommFold}(op,s,comm) = \\mathrm{fold}(op).$$$

Lean4

/-- Fold of a `s : Multiset α` with an associative `op : α → α → α`, given a proofs that `op`
is commutative on all elements `x ∈ s`. -/
def noncommFold (s : Multiset α) (comm : {x | x ∈ s}.Pairwise fun x y => op x y = op y x) : α → α :=
  noncommFoldr op s fun x hx y hy h b => by rw [← assoc.assoc, comm hx hy h, assoc.assoc]

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