Theorems · Theorem · combinatorics

Finset.fold_const

∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {b : β}
  {s : Finset α} [hd : Decidable (s = ∅)] (c : β),
  op c (op b c) = op b c → Finset.fold op b (fun x => c) s = if s = ∅ then b else op b c

Defined in

Mathlib.Data.Finset.Fold

Cited by

1 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Std.CommutativeStd.AssociativeDecidable