Commit 2026-09-02 22:11 c4a007f4

View on Github →

feat(Algebra/Tropical/Basic): split Tropical into MinTropical/MaxTropical (#42076) This PR renames Tropical to MinTropical, and uses to_dual to generate MaxTropical from it. Having both forms available is a lot more convenient than having to work with Tropical (_ᵒᵈ) if you want to use the opposite order.

Estimated changes

added theorem MinTropical.add_eq_iff
added theorem MinTropical.add_pow
added theorem MinTropical.add_self
added theorem MinTropical.inf_eq_add
added theorem MinTropical.le_zero
added theorem MinTropical.min_eq_add
added theorem MinTropical.succ_nsmul
added def MinTropical.trop
added theorem MinTropical.trop_add
added theorem MinTropical.trop_inf
added theorem MinTropical.trop_min
added theorem MinTropical.trop_nsmul
added theorem MinTropical.trop_smul
added theorem MinTropical.trop_top
added theorem MinTropical.trop_zero
added theorem MinTropical.trop_zsmul
added theorem MinTropical.untrop_add
added theorem MinTropical.untrop_div
added theorem MinTropical.untrop_inv
added theorem MinTropical.untrop_max
added theorem MinTropical.untrop_mul
added theorem MinTropical.untrop_one
added theorem MinTropical.untrop_pow
added theorem MinTropical.untrop_sup
added def MinTropical
deleted theorem Tropical.add_eq_iff
deleted theorem Tropical.add_eq_left
deleted theorem Tropical.add_eq_left_iff
deleted theorem Tropical.add_eq_right
deleted theorem Tropical.add_eq_right_iff
deleted theorem Tropical.add_eq_zero_iff
deleted theorem Tropical.add_pow
deleted theorem Tropical.add_self
deleted theorem Tropical.inf_eq_add
deleted theorem Tropical.injective_trop
deleted theorem Tropical.injective_untrop
deleted theorem Tropical.le_zero
deleted theorem Tropical.leftInverse_trop
deleted theorem Tropical.min_eq_add
deleted theorem Tropical.mul_eq_zero_iff
deleted theorem Tropical.succ_nsmul
deleted theorem Tropical.surjective_trop
deleted def Tropical.trop
deleted def Tropical.tropEquiv
deleted theorem Tropical.tropEquiv_coe_fn
deleted def Tropical.tropRec
deleted theorem Tropical.trop_add
deleted theorem Tropical.trop_add_def
deleted theorem Tropical.trop_coe_ne_zero
deleted theorem Tropical.trop_inf
deleted theorem Tropical.trop_inj_iff
deleted theorem Tropical.trop_injective
deleted theorem Tropical.trop_max_def
deleted theorem Tropical.trop_min
deleted theorem Tropical.trop_monotone
deleted theorem Tropical.trop_mul_def
deleted theorem Tropical.trop_nsmul
deleted theorem Tropical.trop_smul
deleted theorem Tropical.trop_sup_def
deleted theorem Tropical.trop_top
deleted theorem Tropical.trop_untrop
deleted theorem Tropical.trop_zero
deleted theorem Tropical.trop_zsmul
deleted def Tropical.untrop
deleted theorem Tropical.untrop_add
deleted theorem Tropical.untrop_div
deleted theorem Tropical.untrop_inj_iff
deleted theorem Tropical.untrop_injective
deleted theorem Tropical.untrop_inv
deleted theorem Tropical.untrop_le_iff
deleted theorem Tropical.untrop_lt_iff
deleted theorem Tropical.untrop_max
deleted theorem Tropical.untrop_monotone
deleted theorem Tropical.untrop_mul
deleted theorem Tropical.untrop_one
deleted theorem Tropical.untrop_pow
deleted theorem Tropical.untrop_sup
deleted theorem Tropical.untrop_trop
deleted theorem Tropical.untrop_zero
deleted theorem Tropical.untrop_zpow
deleted theorem Tropical.zero_ne_trop_coe
deleted theorem Finset.trop_inf
deleted theorem Finset.untrop_sum'
deleted theorem Finset.untrop_sum
deleted theorem List.trop_minimum
deleted theorem List.trop_sum
deleted theorem List.untrop_prod
added theorem MinTropical.trop_iInf
added theorem MinTropical.trop_sum
added theorem MinTropical.untrop_sum
deleted theorem Multiset.trop_inf
deleted theorem Multiset.trop_sum
deleted theorem Multiset.untrop_prod
deleted theorem Multiset.untrop_sum
deleted theorem trop_iInf
deleted theorem trop_sInf_image
deleted theorem trop_sum
deleted theorem untrop_prod
deleted theorem untrop_sum
deleted theorem untrop_sum_eq_sInf_image