Theorem MinTropical.Finset.untrop_sum'

Modification history

2026-09-02 22:11
Mathlib/Algebra/Tropical/BigOperators.lean
feat(Algebra/Tropical/Basic): split `Tropical` into `MinTropical`/`MaxTropical` (#42076) …
Added MinTropical.Finset.untrop_sum'View on Github →