Theorems · Theorem · combinatorics
Multiset.foldr.congr_simp
∀ {α : Type u_1} {β : Type v} (f f_1 : α → β → β) (e_f : f = f_1) [inst : LeftCommutative f] (b b_1 : β),
b = b_1 → ∀ (s s_1 : Multiset α), s = s_1 → Multiset.foldr f b s = Multiset.foldr f_1 b_1 s_1- Defined in
- Mathlib.Data.Multiset.MapFold
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses propext
- Assumes
- LeftCommutative
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Multisetstatement and proof · cited by 2,627
- LeftCommutativestatement and proof · cited by 20
- Multiset.foldrstatement and proof · cited by 18
Cited by1
Results whose statement or proof uses this declaration.
- Polynomial.natDegree_sum_leproof · cited by 9