English
There is an instance asserting that Tropical (WithTop R) has no zero divisors when R is AddCommMonoid.
Русский
Существует экземпляр, подтверждающий отсутствие нулевых делителей в Tropical(WithTop R) при R аддитивном моноиде.
LaTeX
$$$\mathrm{NoZeroDivisors}(\mathrm{Tropical}(\mathrm{WithTop}(R)))$$$
Lean4
theorem trop_sInf_image [ConditionallyCompleteLinearOrder R] (s : Finset S) (f : S → WithTop R) :
trop (sInf (f '' s)) = ∑ i ∈ s, trop (f i) :=
by
rcases s.eq_empty_or_nonempty with (rfl | h)
· simp only [Set.image_empty, coe_empty, sum_empty, WithTop.sInf_empty, trop_top]
rw [← inf'_eq_csInf_image _ h, inf'_eq_inf, s.trop_inf]