untrop_prod — Mathlib

English

For AddMonoid R, untrop of the product of a multiset equals the sum of untrops of its elements.

Русский

Для AddMonoid R untrop произведения мультисета равен сумме untrop элементов мультисета.

LaTeX

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

Lean4

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

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