trop_sum — Mathlib

English

For any additive monoid R, trop of the sum of a list equals the product of trop of elements.

Русский

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

LaTeX

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

Lean4

theorem trop_sum [AddMonoid R] (l : List R) : trop l.sum = List.prod (l.map trop) := by
  induction l with
  | nil => simp
  | cons hd tl IH => simp [← IH]

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