Commit 2023-01-05 12:49 cac724d1

View on Github →

feat: port Algebra.Tropical.Basic (#1165) Main change here was making Tropical irreducible because it seemed to fix things.

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.inf_eq_add
added theorem Tropical.le_zero
added theorem Tropical.min_eq_add
added theorem Tropical.succ_nsmul
added def Tropical.trop
added def Tropical.tropRec
added theorem Tropical.trop_add
added theorem Tropical.trop_add_def
added theorem Tropical.trop_inf
added theorem Tropical.trop_inj_iff
added theorem Tropical.trop_max_def
added theorem Tropical.trop_min
added theorem Tropical.trop_monotone
added theorem Tropical.trop_mul_def
added theorem Tropical.trop_nsmul
added theorem Tropical.trop_smul
added theorem Tropical.trop_sup_def
added theorem Tropical.trop_top
added theorem Tropical.trop_untrop
added theorem Tropical.trop_zero
added theorem Tropical.trop_zsmul
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_lt_iff
added theorem Tropical.untrop_max
added theorem Tropical.untrop_mul
added theorem Tropical.untrop_one
added theorem Tropical.untrop_pow
added theorem Tropical.untrop_sup
added theorem Tropical.untrop_trop
added theorem Tropical.untrop_zero
added theorem Tropical.untrop_zpow
added def Tropical