noncommFold_coe — Mathlib

English

Let l be a list and comm a valid witness for left-commutativity; then noncommFold op (l as multiset) comm a equals l.foldr op a.

Русский

Пусть l — список и comm — корректное доказательство лево-кооммутативности; тогда noncommFold op (l как мультисет) comm a равно l.foldr op a.

LaTeX

$$$\\mathrm{noncommFold}(op,(l:\\mathrm{Multiset}\\alpha),comm,a)=l.foldr(op,a).$$$

Lean4

@[simp]
theorem noncommFold_coe (l : List α) (comm) (a : α) : noncommFold op (l : Multiset α) comm a = l.foldr op a := by
  simp [noncommFold]

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