Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-07 15:17 f8cfed4d

View on Github →

feat(algebra/tropical/basic): define tropical semiring (#8864) Just the initial algebraic structures. Follow up PRs will provide these with a topology, prove that tropical polynomials can be interpreted as sums of affine maps, and further towards tropical geometry.

Estimated changes

added theorem tropical.add_eq_iff
added theorem tropical.add_eq_left
added theorem tropical.add_eq_right
added theorem tropical.add_pow
added theorem tropical.add_self
added theorem tropical.bit0
added theorem tropical.le_zero
added theorem tropical.succ_nsmul
added def tropical.trop
added theorem tropical.trop_add_def
added theorem tropical.trop_inj_iff
added theorem tropical.trop_mul_def
added theorem tropical.trop_nsmul
added theorem tropical.trop_top
added theorem tropical.trop_untrop
added def tropical.untrop
added theorem tropical.untrop_add
added theorem tropical.untrop_div
added theorem tropical.untrop_inv
added theorem tropical.untrop_le_iff
added theorem tropical.untrop_mul
added theorem tropical.untrop_one
added theorem tropical.untrop_pow
added theorem tropical.untrop_trop
added theorem tropical.untrop_zero
added def tropical