Theorem Tropical.tropOrderIso_coe_fn

Modification history

2026-09-02 22:11
Mathlib/Algebra/Tropical/Basic.lean
feat(Algebra/Tropical/Basic): split `Tropical` into `MinTropical`/`MaxTropical` (#42076) …
Deleted Tropical.tropOrderIso_coe_fnView on Github →
2023-01-07 14:35
Mathlib/Algebra/Tropical/Basic.lean
chore: tidy various files (#1412)
Added Tropical.tropOrderIso_coe_fnView on Github →