prod_cons — Mathlib

English

The product over a cons-constructed multiset satisfies the recursion: prod(a :: s) = a · prod s.

Русский

Произведение над мультисетом, построенным через оператор cons, удовлетворяет рекурсию: prod(a :: s) = a · prod s.

LaTeX

$$$\\mathrm{prod}(a ::\\ₘ s) = a \\cdot \\mathrm{prod}~s$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_cons (a : M) (s) : prod (a ::ₘ s) = a * prod s :=
  foldr_cons _ _ _ _

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