noncommFoldr_eq_foldr — Mathlib

English

If the operation is associative and commutative (Std.Commutative), then noncommFold op s comm a equals fold op a s; order independence holds automatically.

Русский

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

LaTeX

$$$\\text{If }[Std.Commutative\\ op],\\; \\mathrm{noncommFold}(op,s,comm) = \\mathrm{fold}(op).$$$

Lean4

theorem noncommFoldr_eq_foldr (s : Multiset α) [h : LeftCommutative f] (b : β) :
    noncommFoldr f s (fun x _ y _ _ => h.left_comm x y) b = foldr f b s :=
  by
  induction s using Quotient.inductionOn
  simp

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