untrop_prod — Mathlib

English

For Tropical R, untrop of the product of a list equals the sum of untrops of the elements.

Русский

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

LaTeX

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

Lean4

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

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