prod_add — Mathlib

English

For any two multisets s and t in a commutative monoid M, prod(s + t) = prod(s) · prod(t).

Русский

Для любых мультимножеств s и t в коммутативном моноиде M верно: prod(s + t) = prod(s) · prod(t).

LaTeX

$$$ \mathrm{prod}(s + t) = \mathrm{prod}(s) \cdot \mathrm{prod}(t) $$$

Lean4

@[to_additive (attr := simp, grind =)]
theorem prod_add (s t : Multiset M) : prod (s + t) = prod s * prod t :=
  Quotient.inductionOn₂ s t fun l₁ l₂ => by simp

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