mathlib

a5f79090 - fix(algebra/tropical/basic): provide explicit min and max (#11380)

fix(algebra/tropical/basic): provide explicit min and max (#11380) This also renames `tropical.add` to `tropical.has_add`, since this matches how we normally do this, and it makes unfolding easier. Without this change, we have a diamond where `linear_order.min` is not defeq to `lattice.inf`.