Theorem Tropical.trop_coe_ne_zero

Modification history

2026-09-02 22:11

Mathlib/Algebra/Tropical/Basic.lean

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

Deleted Tropical.trop_coe_ne_zero View on Github →

2023-01-05 12:49

Mathlib/Algebra/Tropical/Basic.lean

feat: port Algebra.Tropical.Basic (#1165) …

Added Tropical.trop_coe_ne_zero View on Github →