# mathlib3documentation

algebra.tropical.basic

# Tropical algebraic structures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines algebraic structures of the (min-)tropical numbers, up to the tropical semiring. Some basic lemmas about conversion from the base type R to tropical R are provided, as well as the expected implementations of tropical addition and tropical multiplication.

## Main declarations #

• tropical R: The type synonym of the tropical interpretation of R. If [linear_order R], then addition on R is via min.
• semiring (tropical R): A linear_ordered_add_comm_monoid_with_top R induces a semiring (tropical R). If one solely has [linear_ordered_add_comm_monoid R], then the "tropicalization of R" would be tropical (with_top R).

## Implementation notes #

The tropical structure relies on has_top and min. For the max-tropical numbers, use order_dual R.

Inspiration was drawn from the implementation of additive/multiplicative/opposite, where a type synonym is created with some barebones API, and quickly made irreducible.

Algebraic structures are provided with as few typeclass assumptions as possible, even though most references rely on semiring (tropical R) for building up the whole theory.

## References followed #

@[irreducible]
def tropical (R : Type u) :

The tropicalization of a type R.

Equations
• = R
Instances for tropical
def tropical.trop {R : Type u} :
R

Reinterpret x : R as an element of tropical R. See tropical.trop_equiv for the equivalence.

Equations
def tropical.untrop {R : Type u} :
R

Reinterpret x : tropical R as an element of R. See tropical.trop_equiv for the equivalence.

Equations
theorem tropical.trop_injective {R : Type u} :
@[simp]
theorem tropical.trop_inj_iff {R : Type u} (x y : R) :
x = y
@[simp]
theorem tropical.untrop_inj_iff {R : Type u} (x y : tropical R) :
x = y
@[simp]
theorem tropical.trop_untrop {R : Type u} (x : tropical R) :
@[simp]
theorem tropical.untrop_trop {R : Type u} (x : R) :
def tropical.trop_equiv {R : Type u} :
R

Reinterpret x : R as an element of tropical R. See tropical.trop_order_iso for the order-preserving equivalence.

Equations
@[simp]
theorem tropical.trop_equiv_coe_fn {R : Type u} :
@[simp]
theorem tropical.trop_eq_iff_eq_untrop {R : Type u} {x : R} {y : tropical R} :
theorem tropical.untrop_eq_iff_eq_trop {R : Type u} {x : tropical R} {y : R} :
theorem tropical.injective_trop {R : Type u} :
theorem tropical.surjective_trop {R : Type u} :
@[protected, instance]
def tropical.inhabited {R : Type u} [inhabited R] :
Equations
@[simp]
def tropical.trop_rec {R : Type u} {F : Sort v} (h : Π (X : R), F ) (X : tropical R) :
F X

Recursing on a x' : tropical R is the same as recursing on an x : R reinterpreted as a term of tropical R via trop x.

Equations
@[protected, instance]
Equations
@[protected, instance]
def tropical.has_le {R : Type u} [has_le R] :
Equations
@[simp]
theorem tropical.untrop_le_iff {R : Type u} [has_le R] {x y : tropical R} :
x y
@[protected, instance]
def tropical.decidable_le {R : Type u} [has_le R]  :
Equations
@[protected, instance]
def tropical.has_lt {R : Type u} [has_lt R] :
Equations
@[simp]
theorem tropical.untrop_lt_iff {R : Type u} [has_lt R] {x y : tropical R} :
x < y
@[protected, instance]
def tropical.decidable_lt {R : Type u} [has_lt R]  :
Equations
@[protected, instance]
Equations
def tropical.trop_order_iso {R : Type u} [preorder R] :
R ≃o

Reinterpret x : R as an element of tropical R, preserving the order.

Equations
@[simp]
@[simp]
theorem tropical.trop_monotone {R : Type u} [preorder R] :
theorem tropical.untrop_monotone {R : Type u} [preorder R] :
@[protected, instance]
def tropical.partial_order {R : Type u}  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def tropical.has_top {R : Type u} [has_top R] :
Equations
@[simp]
theorem tropical.untrop_zero {R : Type u} [has_top R] :
@[simp]
theorem tropical.trop_top {R : Type u} [has_top R] :
@[simp]
theorem tropical.trop_coe_ne_zero {R : Type u} (x : R) :
@[simp]
theorem tropical.zero_ne_trop_coe {R : Type u} (x : R) :
@[simp]
theorem tropical.le_zero {R : Type u} [has_le R] [order_top R] (x : tropical R) :
x 0
@[protected, instance]
def tropical.order_top {R : Type u} [has_le R] [order_top R] :
Equations
@[protected, instance]

Tropical addition is the minimum of two underlying elements of R.

Equations
@[protected, instance]
Equations
@[simp]
theorem tropical.untrop_add {R : Type u} [linear_order R] (x y : tropical R) :
@[simp]
theorem tropical.trop_min {R : Type u} [linear_order R] (x y : R) :
@[simp]
theorem tropical.trop_inf {R : Type u} [linear_order R] (x y : R) :
theorem tropical.trop_add_def {R : Type u} [linear_order R] (x y : tropical R) :
x + y =
@[protected, instance]
Equations
@[simp]
theorem tropical.untrop_sup {R : Type u} [linear_order R] (x y : tropical R) :
@[simp]
theorem tropical.untrop_max {R : Type u} [linear_order R] (x y : tropical R) :
@[simp]
theorem tropical.min_eq_add {R : Type u} [linear_order R] :
@[simp]
theorem tropical.inf_eq_add {R : Type u} [linear_order R] :
theorem tropical.trop_max_def {R : Type u} [linear_order R] (x y : tropical R) :
theorem tropical.trop_sup_def {R : Type u} [linear_order R] (x y : tropical R) :
x y =
@[simp]
theorem tropical.add_eq_left {R : Type u} [linear_order R] ⦃x y : tropical R⦄ (h : x y) :
x + y = x
@[simp]
theorem tropical.add_eq_right {R : Type u} [linear_order R] ⦃x y : tropical R⦄ (h : y x) :
x + y = y
theorem tropical.add_eq_left_iff {R : Type u} [linear_order R] {x y : tropical R} :
x + y = x x y
theorem tropical.add_eq_right_iff {R : Type u} [linear_order R] {x y : tropical R} :
x + y = y y x
@[simp]
theorem tropical.add_self {R : Type u} [linear_order R] (x : tropical R) :
x + x = x
@[simp]
theorem tropical.bit0 {R : Type u} [linear_order R] (x : tropical R) :
bit0 x = x
theorem tropical.add_eq_iff {R : Type u} [linear_order R] {x y z : tropical R} :
x + y = z x = z x y y = z y x
@[simp]
theorem tropical.add_eq_zero_iff {R : Type u} [linear_order R] {a b : tropical (with_top R)} :
a + b = 0 a = 0 b = 0
@[protected, instance]
Equations
@[protected, instance]
def tropical.has_mul {R : Type u} [has_add R] :

Tropical multiplication is the addition in the underlying R.

Equations
@[simp]
theorem tropical.trop_add {R : Type u} [has_add R] (x y : R) :
@[simp]
theorem tropical.untrop_mul {R : Type u} [has_add R] (x y : tropical R) :
theorem tropical.trop_mul_def {R : Type u} [has_add R] (x y : tropical R) :
x * y =
@[protected, instance]
def tropical.has_one {R : Type u} [has_zero R] :
Equations
@[simp]
theorem tropical.trop_zero {R : Type u} [has_zero R] :
@[simp]
theorem tropical.untrop_one {R : Type u} [has_zero R] :
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
def tropical.has_inv {R : Type u} [has_neg R] :
Equations
@[simp]
theorem tropical.untrop_inv {R : Type u} [has_neg R] (x : tropical R) :
@[protected, instance]
def tropical.has_div {R : Type u} [has_sub R] :
Equations
@[simp]
theorem tropical.untrop_div {R : Type u} [has_sub R] (x y : tropical R) :
@[protected, instance]
def tropical.semigroup {R : Type u}  :
Equations
@[protected, instance]
def tropical.comm_semigroup {R : Type u}  :
Equations
@[protected, instance]
def tropical.has_pow {R : Type u} {α : Type u_1} [ R] :
Equations
@[simp]
theorem tropical.untrop_pow {R : Type u} {α : Type u_1} [ R] (x : tropical R) (n : α) :
@[simp]
theorem tropical.trop_smul {R : Type u} {α : Type u_1} [ R] (x : R) (n : α) :
@[protected, instance]
def tropical.mul_one_class {R : Type u}  :
Equations
@[protected, instance]
def tropical.monoid {R : Type u} [add_monoid R] :
Equations
@[simp]
theorem tropical.trop_nsmul {R : Type u} [add_monoid R] (x : R) (n : ) :
@[protected, instance]
def tropical.comm_monoid {R : Type u}  :
Equations
@[protected, instance]
def tropical.group {R : Type u} [add_group R] :
Equations
@[protected, instance]
def tropical.comm_group {R : Type u}  :
Equations
@[simp]
theorem tropical.untrop_zpow {R : Type u} [add_group R] (x : tropical R) (n : ) :
@[simp]
theorem tropical.trop_zsmul {R : Type u} [add_group R] (x : R) (n : ) :
@[protected, instance]
def tropical.covariant_mul {R : Type u} [has_le R] [has_add R]  :
@[protected, instance]
@[protected, instance]
@[protected, instance]
def tropical.covariant_mul_lt {R : Type u} [has_lt R] [has_add R]  :
@[protected, instance]
@[protected, instance]
Equations
@[simp]
theorem tropical.add_pow {R : Type u} [linear_order R] [add_monoid R] (x y : tropical R) (n : ) :
(x + y) ^ n = x ^ n + y ^ n
@[protected, instance]
Equations
@[simp]
theorem tropical.succ_nsmul {R : Type u_1} [linear_order R] [order_top R] (x : tropical R) (n : ) :
(n + 1) x = x
@[simp]
theorem tropical.mul_eq_zero_iff {R : Type u_1} {a b : tropical (with_top R)} :
a * b = 0 a = 0 b = 0
@[protected, instance]
def tropical.no_zero_divisors {R : Type u_1}  :