Theorem MinTropical.untrop_lt_iff

Modification history

2026-09-02 22:11

Mathlib/Algebra/Tropical/Basic.lean

feat(Algebra/Tropical/Basic): split `Tropical` into `MinTropical`/`MaxTropical` (#42076) …

Added MinTropical.untrop_lt_iff View on Github →