trop_sum — Mathlib

English

For any AddCommMonoid R, trop of the Finset sum equals the Finset product of trop(f(i)).

Русский

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

LaTeX

$$$\forall s \in \mathrm{Finset}\,S,\ \operatorname{trop}\left(\sum_{i \in s} f(i)\right) = \prod_{i \in s} \operatorname{trop}(f(i))$$$

Lean4

theorem trop_sum [AddCommMonoid R] (s : Finset S) (f : S → R) : trop (∑ i ∈ s, f i) = ∏ i ∈ s, trop (f i) :=
  by
  convert Multiset.trop_sum (s.val.map f)
  simp only [Multiset.map_map, Function.comp_apply]
  rfl

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