Mathlib Map

Theorems · Theorem · combinatorics

Finset.fold.congr_simp

∀ {α : Type u_1} {β : Type u_2} (op op_1 : β → β → β) (e_op : op = op_1) [hc : Std.Commutative op]
  [ha : Std.Associative op] (b b_1 : β),
  b = b_1 →
    ∀ (f f_1 : α → β), f = f_1 → ∀ (s s_1 : Finset α), s = s_1 → Finset.fold op b f s = Finset.fold op_1 b_1 f_1 s_1
Defined in
Mathlib.Data.Finset.Fold
Cited by
2 results in Mathlib
Foundations
Depth 14 from the axioms · uses propext, Quot.sound
Assumes
Std.CommutativeStd.Associative
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Finset.fold_insert_idem · cited by 5Finset.fold_insert_idemFinset.fold_ite' · cited by 1Finset.fold_ite'Finset · cited by 13712FinsetFinset.fold · cited by 46Finset.foldfold.congr_simpCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Finsetstatement and proof · cited by 13,712
  • Finset.foldstatement and proof · cited by 46

Cited by2

Results whose statement or proof uses this declaration.