Commit 2021-12-02 23:23 c791747d

View on Github →

feat(algebra/tropical/basic): various API (#10487) Generalize some order instance to just require has_le of the base R. (un)trop_monotone trop_(min|inf) iffs between addition and order tropical.add_comm_monoid (in parallel to #10486) (co|contra)variant instances

Estimated changes

Modified src/algebra/tropical/basic.lean

added theorem tropical.add_eq_left_iff

added theorem tropical.add_eq_right_iff

modified theorem tropical.le_zero

modified theorem tropical.succ_nsmul

added theorem tropical.trop_add

added theorem tropical.trop_inf

added theorem tropical.trop_min

added theorem tropical.trop_monotone

added theorem tropical.trop_zero

added theorem tropical.trop_zsmul

modified theorem tropical.untrop_le_iff

added theorem tropical.untrop_lt_iff

added theorem tropical.untrop_monotone

modified theorem tropical.untrop_one

added theorem tropical.untrop_zpow