trop_sum — Mathlib

English

For any AddCommMonoid R, trop of the sum of a multiset equals the product of trop of its mapped elements.

Русский

Для любого AddCommMonoid R trop суммы мультисет равен произведению trop отображений элементов мультисе-та.

LaTeX

$$$\forall s \in \mathrm{Multiset}\,R,\ \operatorname{trop}(\mathrm{sum}\,s) = \mathrm{prod}(\mathrm{map}\,\operatorname{trop}\,s)$$$

Lean4

theorem trop_sum [AddCommMonoid R] (s : Multiset R) : trop s.sum = Multiset.prod (s.map trop) :=
  Quotient.inductionOn s (by simpa using List.trop_sum)

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