prod_add — Mathlib

English

The product of the sum of two prime multisets equals the product of the first times the product of the second.

Русский

Произведение суммы двух мультимножест PrimeMultiset равняется произведению первого на произведение второго.

LaTeX

$$$ (u + v).prod = u.prod \\cdot v.prod $$$

Lean4

theorem prod_add (u v : PrimeMultiset) : (u + v).prod = u.prod * v.prod :=
  by
  change (coePNatMonoidHom (u + v)).prod = _
  rw [coePNatMonoidHom.map_add]
  exact Multiset.prod_add _ _

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