Documentation

Mathlib.Algebra.Tropical.Basic

Tropical algebraic structures #

This file defines algebraic structures of the min/max-tropical numbers, up to the tropical semiring. All declarations about MinTropical are translated to MaxTropical using to_dual. Some basic lemmas about conversion from the base type R to MinTropical R/MaxTropical R are provided, as well as the expected implementations of tropical addition and tropical multiplication.

Main declarations #

MinTropical R: The type synonym of the tropical interpretation of R. If [LinearOrder R], then addition on R is via min.
Semiring (MinTropical R): A LinearOrderedAddCommMonoidWithTop R induces a Semiring (MinTropical R). If one solely has [LinearOrderedAddCommMonoid R], then the "tropicalization of R" would be MinTropical (WithTop R).

Implementation notes #

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 (MinTropical R) for building up the whole theory.

References followed #

https://arxiv.org/pdf/math/0408099.pdf
https://www.mathenjeans.fr/sites/default/files/sujets/tropical_geometry_-_casagrande.pdf

@[irreducible]

def MinTropical (R : Type u) :

The min-tropicalization of a type R.

Equations

MinTropical R = R

Instances For

@[irreducible]

def MaxTropical (R : Type u) :

The max-tropicalization of a type R.

Equations

MaxTropical R = R

Instances For

@[deprecated MinTropical (since := "2026-07-24")]

def Tropical (R : Type u) :

The min-tropicalization of a type R.

Equations

Tropical R = R

Instances For

def MinTropical.trop {R : Type u} :

R → MinTropical R

Reinterpret x : R as an element of MinTropical R. See MinTropical.tropEquiv for the equivalence.

Equations

MinTropical.trop = id

Instances For

def MaxTropical.trop {R : Type u} :

R → MaxTropical R

Reinterpret x : R as an element of MaxTropical R. See MaxTropical.tropEquiv for the equivalence.

Equations

MaxTropical.trop = id

Instances For

def MinTropical.untrop {R : Type u} :

MinTropical R → R

Reinterpret x : MinTropical R as an element of R. See MinTropical.tropEquiv for the equivalence.

Equations

MinTropical.untrop = id

Instances For

def MaxTropical.untrop {R : Type u} :

MaxTropical R → R

Reinterpret x : MaxTropical R as an element of R. See MaxTropical.tropEquiv for the equivalence.

Equations

MaxTropical.untrop = id

Instances For

theorem MinTropical.trop_injective {R : Type u} :

Function.Injective trop

theorem MaxTropical.trop_injective {R : Type u} :

Function.Injective trop

theorem MinTropical.untrop_injective {R : Type u} :

Function.Injective untrop

theorem MaxTropical.untrop_injective {R : Type u} :

Function.Injective untrop

@[simp]

theorem MinTropical.trop_inj_iff {R : Type u} (x y : R) :

trop x = trop y ↔ x = y

@[simp]

theorem MaxTropical.trop_inj_iff {R : Type u} (x y : R) :

trop x = trop y ↔ x = y

@[simp]

theorem MinTropical.untrop_inj_iff {R : Type u} (x y : MinTropical R) :

untrop x = untrop y ↔ x = y

@[simp]

theorem MaxTropical.untrop_inj_iff {R : Type u} (x y : MaxTropical R) :

untrop x = untrop y ↔ x = y

@[simp]

theorem MinTropical.trop_untrop {R : Type u} (x : MinTropical R) :

trop (untrop x) = x

@[simp]

theorem MaxTropical.trop_untrop {R : Type u} (x : MaxTropical R) :

trop (untrop x) = x

@[simp]

theorem MinTropical.untrop_trop {R : Type u} (x : R) :

untrop (trop x) = x

@[simp]

theorem MaxTropical.untrop_trop {R : Type u} (x : R) :

untrop (trop x) = x

theorem MinTropical.leftInverse_trop {R : Type u} :

Function.LeftInverse trop untrop

theorem MaxTropical.leftInverse_trop {R : Type u} :

Function.LeftInverse trop untrop

theorem MinTropical.rightInverse_trop {R : Type u} :

Function.RightInverse trop untrop

theorem MaxTropical.rightInverse_trop {R : Type u} :

Function.RightInverse trop untrop

def MinTropical.tropEquiv {R : Type u} :

R ≃ MinTropical R

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

Equations

MinTropical.tropEquiv = { toFun := MinTropical.trop, invFun := MinTropical.untrop, left_inv := ⋯, right_inv := ⋯ }

Instances For

def MaxTropical.tropEquiv {R : Type u} :

R ≃ MaxTropical R

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

Equations

MaxTropical.tropEquiv = { toFun := MaxTropical.trop, invFun := MaxTropical.untrop, left_inv := ⋯, right_inv := ⋯ }

Instances For

@[simp]

theorem MinTropical.tropEquiv_coe_fn {R : Type u} :

⇑tropEquiv = trop

@[simp]

theorem MaxTropical.tropEquiv_coe_fn {R : Type u} :

⇑tropEquiv = trop

@[simp]

theorem MinTropical.tropEquiv_symm_coe_fn {R : Type u} :

⇑tropEquiv.symm = untrop

@[simp]

theorem MaxTropical.tropEquiv_symm_coe_fn {R : Type u} :

⇑tropEquiv.symm = untrop

theorem MinTropical.trop_eq_iff_eq_untrop {R : Type u} {x : R} {y : MinTropical R} :

trop x = y ↔ x = untrop y

theorem MaxTropical.trop_eq_iff_eq_untrop {R : Type u} {x : R} {y : MaxTropical R} :

trop x = y ↔ x = untrop y

theorem MinTropical.untrop_eq_iff_eq_trop {R : Type u} {x : MinTropical R} {y : R} :

untrop x = y ↔ x = trop y

theorem MaxTropical.untrop_eq_iff_eq_trop {R : Type u} {x : MaxTropical R} {y : R} :

untrop x = y ↔ x = trop y

theorem MinTropical.injective_trop {R : Type u} :

Function.Injective trop

theorem MaxTropical.injective_trop {R : Type u} :

Function.Injective trop

theorem MinTropical.injective_untrop {R : Type u} :

Function.Injective untrop

theorem MaxTropical.injective_untrop {R : Type u} :

Function.Injective untrop

theorem MinTropical.surjective_trop {R : Type u} :

Function.Surjective trop

theorem MaxTropical.surjective_trop {R : Type u} :

Function.Surjective trop

theorem MinTropical.surjective_untrop {R : Type u} :

Function.Surjective untrop

theorem MaxTropical.surjective_untrop {R : Type u} :

Function.Surjective untrop

@[instance_reducible]

instance MinTropical.instInhabited {R : Type u} [Inhabited R] :

Inhabited (MinTropical R)

Equations

MinTropical.instInhabited = { default := MinTropical.trop default }

@[instance_reducible]

instance MaxTropical.instInhabited {R : Type u} [Inhabited R] :

Inhabited (MaxTropical R)

Equations

MaxTropical.instInhabited = { default := MaxTropical.trop default }

def MinTropical.tropRec {R : Type u} {F : MinTropical R → Sort v} (h : (X : R) → F (trop X)) (X : MinTropical R) :

F X

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

Equations

MinTropical.tropRec h X = h (MinTropical.untrop X)

Instances For

def MaxTropical.tropRec {R : Type u} {F : MaxTropical R → Sort v} (h : (X : R) → F (trop X)) (X : MaxTropical R) :

F X

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

Equations

MaxTropical.tropRec h X = h (MaxTropical.untrop X)

Instances For

@[instance_reducible]

instance MinTropical.instDecidableEq {R : Type u} [DecidableEq R] :

DecidableEq (MinTropical R)

Equations

x✝¹.instDecidableEq x✝ = decidable_of_iff (MinTropical.untrop x✝¹ = MinTropical.untrop x✝) ⋯

@[instance_reducible]

instance MaxTropical.instDecidableEq {R : Type u} [DecidableEq R] :

DecidableEq (MaxTropical R)

Equations

x✝¹.instDecidableEq x✝ = decidable_of_iff (MaxTropical.untrop x✝¹ = MaxTropical.untrop x✝) ⋯

@[instance_reducible]

instance MinTropical.instLE {R : Type u} [LE R] :

LE (MinTropical R)

Equations

MinTropical.instLE = { le := fun (x y : MinTropical R) => MinTropical.untrop x ≤ MinTropical.untrop y }

@[instance_reducible]

instance MaxTropical.instLE {R : Type u} [LE R] :

LE (MaxTropical R)

Equations

MaxTropical.instLE = { le := fun (y x : MaxTropical R) => MaxTropical.untrop y ≤ MaxTropical.untrop x }

@[simp]

theorem MinTropical.untrop_le_iff {R : Type u} [LE R] {x y : MinTropical R} :

untrop x ≤ untrop y ↔ x ≤ y

@[simp]

theorem MaxTropical.untrop_le_iff {R : Type u} [LE R] {x y : MaxTropical R} :

untrop y ≤ untrop x ↔ y ≤ x

@[instance_reducible]

instance MinTropical.instDecidableLE {R : Type u} [LE R] [DecidableLE R] :

DecidableLE (MinTropical R)

Equations

MinTropical.instDecidableLE = MinTropical.instDecidableLE._aux_1

@[instance_reducible]

instance MaxTropical.instDecidableLE {R : Type u} [LE R] [DecidableLE R] :

DecidableLE (MaxTropical R)

Equations

MaxTropical.instDecidableLE = MaxTropical.instDecidableLE._aux_1

@[instance_reducible]

instance MinTropical.instLT {R : Type u} [LT R] :

LT (MinTropical R)

Equations

MinTropical.instLT = { lt := fun (x y : MinTropical R) => MinTropical.untrop x < MinTropical.untrop y }

@[instance_reducible]

instance MaxTropical.instLT {R : Type u} [LT R] :

LT (MaxTropical R)

Equations

MaxTropical.instLT = { lt := fun (y x : MaxTropical R) => MaxTropical.untrop y < MaxTropical.untrop x }

@[simp]

theorem MinTropical.untrop_lt_iff {R : Type u} [LT R] {x y : MinTropical R} :

untrop x < untrop y ↔ x < y

@[simp]

theorem MaxTropical.untrop_lt_iff {R : Type u} [LT R] {x y : MaxTropical R} :

untrop y < untrop x ↔ y < x

@[instance_reducible]

instance MinTropical.instDecidableLT {R : Type u} [LT R] [DecidableLT R] :

DecidableLT (MinTropical R)

Equations

MinTropical.instDecidableLT = MinTropical.instDecidableLT._aux_1

@[instance_reducible]

instance MaxTropical.instDecidableLT {R : Type u} [LT R] [DecidableLT R] :

DecidableLT (MaxTropical R)

Equations

MaxTropical.instDecidableLT = MaxTropical.instDecidableLT._aux_1

@[instance_reducible]

instance MinTropical.instPreorder {R : Type u} [Preorder R] :

Preorder (MinTropical R)

Equations

MinTropical.instPreorder = { toLE := MinTropical.instLE, toLT := MinTropical.instLT, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

@[instance_reducible]

instance MaxTropical.instPreorder {R : Type u} [Preorder R] :

Preorder (MaxTropical R)

Equations

MaxTropical.instPreorder = { toLE := MaxTropical.instLE, toLT := MaxTropical.instLT, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

def MinTropical.tropOrderIso {R : Type u} [Preorder R] :

R ≃o MinTropical R

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

Equations

MinTropical.tropOrderIso = { toEquiv := MinTropical.tropEquiv, map_rel_iff' := ⋯ }

Instances For

def MaxTropical.tropOrderIso {R : Type u} [Preorder R] :

R ≃o MaxTropical R

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

Equations

MaxTropical.tropOrderIso = { toEquiv := (let __src := MaxTropical.tropEquiv; { toEquiv := __src, map_rel_iff' := ⋯ }).toEquiv, map_rel_iff' := ⋯ }

Instances For

@[simp]

theorem MinTropical.tropOrderIso_coe_fn {R : Type u} [Preorder R] :

⇑tropOrderIso = trop

@[simp]

theorem MaxTropical.tropOrderIso_coe_fn {R : Type u} [Preorder R] :

⇑tropOrderIso = trop

@[simp]

theorem MinTropical.tropOrderIso_symm_coe_fn {R : Type u} [Preorder R] :

⇑tropOrderIso.symm = untrop

@[simp]

theorem MaxTropical.tropOrderIso_symm_coe_fn {R : Type u} [Preorder R] :

⇑tropOrderIso.symm = untrop

theorem MinTropical.trop_monotone {R : Type u} [Preorder R] :

theorem MaxTropical.trop_monotone {R : Type u} [Preorder R] :

theorem MinTropical.untrop_monotone {R : Type u} [Preorder R] :

Monotone untrop

theorem MaxTropical.untrop_monotone {R : Type u} [Preorder R] :

Monotone untrop

@[instance_reducible]

instance MinTropical.instPartialOrder {R : Type u} [PartialOrder R] :

PartialOrder (MinTropical R)

Equations

MinTropical.instPartialOrder = { toPreorder := MinTropical.instPreorder, le_antisymm := ⋯ }

@[instance_reducible]

instance MaxTropical.instPartialOrder {R : Type u} [PartialOrder R] :

PartialOrder (MaxTropical R)

Equations

MaxTropical.instPartialOrder = { toPreorder := MaxTropical.instPreorder, le_antisymm := ⋯ }

@[instance_reducible]

instance MinTropical.instZeroOfTop {R : Type u} [Top R] :

Zero (MinTropical R)

Equations

MinTropical.instZeroOfTop = { zero := MinTropical.trop ⊤ }

@[instance_reducible]

instance MaxTropical.instZeroOfBot {R : Type u} [Bot R] :

Zero (MaxTropical R)

Equations

MaxTropical.instZeroOfBot = { zero := MaxTropical.trop ⊥ }

@[instance_reducible]

instance MinTropical.instTop {R : Type u} [Top R] :

Top (MinTropical R)

Equations

MinTropical.instTop = { top := 0 }

@[instance_reducible]

instance MaxTropical.instBot {R : Type u} [Bot R] :

Bot (MaxTropical R)

Equations

MaxTropical.instBot = { bot := 0 }

@[simp]

theorem MinTropical.untrop_zero {R : Type u} [Top R] :

@[simp]

theorem MaxTropical.untrop_zero {R : Type u} [Bot R] :

@[simp]

theorem MinTropical.trop_top {R : Type u} [Top R] :

@[simp]

theorem MaxTropical.trop_bot {R : Type u} [Bot R] :

@[simp]

theorem MinTropical.trop_coe_ne_zero {R : Type u} (x : R) :

trop ↑x ≠ 0

@[simp]

theorem MaxTropical.trop_coe_ne_zero {R : Type u} (x : R) :

trop ↑x ≠ 0

@[simp]

theorem MinTropical.zero_ne_trop_coe {R : Type u} (x : R) :

0 ≠ trop ↑x

@[simp]

theorem MaxTropical.zero_ne_trop_coe {R : Type u} (x : R) :

0 ≠ trop ↑x

@[simp]

theorem MinTropical.le_zero {R : Type u} [LE R] [OrderTop R] (x : MinTropical R) :

x ≤ 0

@[simp]

theorem MaxTropical.le_zero {R : Type u} [LE R] [OrderBot R] (x : MaxTropical R) :

0 ≤ x

@[instance_reducible]

instance MinTropical.instOrderTop {R : Type u} [LE R] [OrderTop R] :

OrderTop (MinTropical R)

Equations

MinTropical.instOrderTop = { toTop := MinTropical.instTop, le_top := ⋯ }

@[instance_reducible]

instance MaxTropical.instOrderBot {R : Type u} [LE R] [OrderBot R] :

OrderBot (MaxTropical R)

Equations

MaxTropical.instOrderBot = { toBot := MaxTropical.instBot, bot_le := ⋯ }

@[instance_reducible]

instance MinTropical.instAdd {R : Type u} [LinearOrder R] :

Add (MinTropical R)

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

Equations

MinTropical.instAdd = { add := fun (x y : MinTropical R) => MinTropical.trop (min (MinTropical.untrop x) (MinTropical.untrop y)) }

@[instance_reducible]

instance MaxTropical.instAdd {R : Type u} [LinearOrder R] :

Add (MaxTropical R)

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

Equations

MaxTropical.instAdd = { add := fun (x y : MaxTropical R) => MaxTropical.trop (max (MaxTropical.untrop x) (MaxTropical.untrop y)) }

@[instance_reducible]

instance MinTropical.instAddCommSemigroup {R : Type u} [LinearOrder R] :

AddCommSemigroup (MinTropical R)

Equations

MinTropical.instAddCommSemigroup = { toAdd := MinTropical.instAdd, add_assoc := ⋯, add_comm := ⋯ }

@[instance_reducible]

instance MaxTropical.instAddCommSemigroup {R : Type u} [LinearOrder R] :

AddCommSemigroup (MaxTropical R)

Equations

MaxTropical.instAddCommSemigroup = { toAdd := MaxTropical.instAdd, add_assoc := ⋯, add_comm := ⋯ }

@[simp]

theorem MinTropical.untrop_add {R : Type u} [LinearOrder R] (x y : MinTropical R) :

untrop (x + y) = min (untrop x) (untrop y)

@[simp]

theorem MaxTropical.untrop_add {R : Type u} [LinearOrder R] (x y : MaxTropical R) :

untrop (x + y) = max (untrop x) (untrop y)

@[simp]

theorem MinTropical.trop_min {R : Type u} [LinearOrder R] (x y : R) :

trop (min x y) = trop x + trop y

@[simp]

theorem MaxTropical.trop_max {R : Type u} [LinearOrder R] (x y : R) :

trop (max x y) = trop x + trop y

@[simp]

theorem MinTropical.trop_inf {R : Type u} [LinearOrder R] (x y : R) :

trop (min x y) = trop x + trop y

@[simp]

theorem MaxTropical.trop_sup {R : Type u} [LinearOrder R] (x y : R) :

trop (max x y) = trop x + trop y

theorem MinTropical.trop_add_def {R : Type u} [LinearOrder R] (x y : MinTropical R) :

x + y = trop (min (untrop x) (untrop y))

theorem MaxTropical.trop_add_def {R : Type u} [LinearOrder R] (x y : MaxTropical R) :

x + y = trop (max (untrop x) (untrop y))

@[instance_reducible]

instance MinTropical.instLinearOrder {R : Type u} [LinearOrder R] :

LinearOrder (MinTropical R)

Equations

One or more equations did not get rendered due to their size.

@[instance_reducible]

instance MaxTropical.instLinearOrder {R : Type u} [LinearOrder R] :

LinearOrder (MaxTropical R)

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem MinTropical.untrop_sup {R : Type u} [LinearOrder R] (x y : MinTropical R) :

untrop (max x y) = max (untrop x) (untrop y)

@[simp]

theorem MaxTropical.untrop_inf {R : Type u} [LinearOrder R] (x y : MaxTropical R) :

untrop (min x y) = min (untrop x) (untrop y)

@[simp]

theorem MinTropical.untrop_max {R : Type u} [LinearOrder R] (x y : MinTropical R) :

untrop (max x y) = max (untrop x) (untrop y)

@[simp]

theorem MaxTropical.untrop_min {R : Type u} [LinearOrder R] (x y : MaxTropical R) :

untrop (min x y) = min (untrop x) (untrop y)

@[simp]

theorem MinTropical.min_eq_add {R : Type u} [LinearOrder R] :

min = fun (x1 x2 : MinTropical R) => x1 + x2

@[simp]

theorem MaxTropical.max_eq_add {R : Type u} [LinearOrder R] :

max = fun (x1 x2 : MaxTropical R) => x1 + x2

@[simp]

theorem MinTropical.inf_eq_add {R : Type u} [LinearOrder R] :

(fun (x1 x2 : MinTropical R) => min x1 x2) = fun (x1 x2 : MinTropical R) => x1 + x2

@[simp]

theorem MaxTropical.sup_eq_add {R : Type u} [LinearOrder R] :

(fun (x1 x2 : MaxTropical R) => max x1 x2) = fun (x1 x2 : MaxTropical R) => x1 + x2

theorem MinTropical.trop_max_def {R : Type u} [LinearOrder R] (x y : MinTropical R) :

max x y = trop (max (untrop x) (untrop y))

theorem MaxTropical.trop_min_def {R : Type u} [LinearOrder R] (x y : MaxTropical R) :

min x y = trop (min (untrop x) (untrop y))

theorem MinTropical.trop_sup_def {R : Type u} [LinearOrder R] (x y : MinTropical R) :

max x y = trop (max (untrop x) (untrop y))

theorem MaxTropical.trop_inf_def {R : Type u} [LinearOrder R] (x y : MaxTropical R) :

min x y = trop (min (untrop x) (untrop y))

@[simp]

theorem MinTropical.add_eq_left {R : Type u} [LinearOrder R] ⦃x y : MinTropical R⦄ (h : x ≤ y) :

x + y = x

@[simp]

theorem MaxTropical.add_eq_left {R : Type u} [LinearOrder R] ⦃x y : MaxTropical R⦄ (h : y ≤ x) :

x + y = x

@[simp]

theorem MinTropical.add_eq_right {R : Type u} [LinearOrder R] ⦃x y : MinTropical R⦄ (h : y ≤ x) :

x + y = y

@[simp]

theorem MaxTropical.add_eq_right {R : Type u} [LinearOrder R] ⦃x y : MaxTropical R⦄ (h : x ≤ y) :

x + y = y

theorem MinTropical.add_eq_left_iff {R : Type u} [LinearOrder R] {x y : MinTropical R} :

x + y = x ↔ x ≤ y

theorem MaxTropical.add_eq_left_iff {R : Type u} [LinearOrder R] {x y : MaxTropical R} :

x + y = x ↔ y ≤ x

theorem MinTropical.add_eq_right_iff {R : Type u} [LinearOrder R] {x y : MinTropical R} :

x + y = y ↔ y ≤ x

theorem MaxTropical.add_eq_right_iff {R : Type u} [LinearOrder R] {x y : MaxTropical R} :

x + y = y ↔ x ≤ y

theorem MinTropical.add_self {R : Type u} [LinearOrder R] (x : MinTropical R) :

x + x = x

theorem MaxTropical.add_self {R : Type u} [LinearOrder R] (x : MaxTropical R) :

x + x = x

theorem MinTropical.add_eq_iff {R : Type u} [LinearOrder R] {x y z : MinTropical R} :

x + y = z ↔ x = z ∧ x ≤ y ∨ y = z ∧ y ≤ x

theorem MaxTropical.add_eq_iff {R : Type u} [LinearOrder R] {x y z : MaxTropical R} :

x + y = z ↔ x = z ∧ y ≤ x ∨ y = z ∧ x ≤ y

@[simp]

theorem MinTropical.add_eq_zero_iff {R : Type u} [LinearOrder R] {a b : MinTropical (WithTop R)} :

a + b = 0 ↔ a = 0 ∧ b = 0

@[simp]

theorem MaxTropical.add_eq_zero_iff {R : Type u} [LinearOrder R] {a b : MaxTropical (WithBot R)} :

a + b = 0 ↔ a = 0 ∧ b = 0

@[instance_reducible]

instance MinTropical.instAddCommMonoidOfOrderTop {R : Type u} [LinearOrder R] [OrderTop R] :

AddCommMonoid (MinTropical R)

Equations

One or more equations did not get rendered due to their size.

@[instance_reducible]

instance MaxTropical.instAddCommMonoidOfOrderBot {R : Type u} [LinearOrder R] [OrderBot R] :

AddCommMonoid (MaxTropical R)

Equations

One or more equations did not get rendered due to their size.

@[instance_reducible]

instance MinTropical.instMulOfAdd {R : Type u} [Add R] :

Mul (MinTropical R)

Tropical multiplication is the addition in the underlying R.

Equations

MinTropical.instMulOfAdd = { mul := fun (x y : MinTropical R) => MinTropical.trop (MinTropical.untrop x + MinTropical.untrop y) }

@[instance_reducible]

instance MaxTropical.instMulOfAdd {R : Type u} [Add R] :

Mul (MaxTropical R)

Tropical multiplication is the addition in the underlying R.

Equations

MaxTropical.instMulOfAdd = { mul := fun (x y : MaxTropical R) => MaxTropical.trop (MaxTropical.untrop x + MaxTropical.untrop y) }

@[simp]

theorem MinTropical.trop_add {R : Type u} [Add R] (x y : R) :

trop (x + y) = trop x * trop y

@[simp]

theorem MaxTropical.trop_add {R : Type u} [Add R] (x y : R) :

trop (x + y) = trop x * trop y

@[simp]

theorem MinTropical.untrop_mul {R : Type u} [Add R] (x y : MinTropical R) :

untrop (x * y) = untrop x + untrop y

@[simp]

theorem MaxTropical.untrop_mul {R : Type u} [Add R] (x y : MaxTropical R) :

untrop (x * y) = untrop x + untrop y

theorem MinTropical.trop_mul_def {R : Type u} [Add R] (x y : MinTropical R) :

x * y = trop (untrop x + untrop y)

theorem MaxTropical.trop_mul_def {R : Type u} [Add R] (x y : MaxTropical R) :

x * y = trop (untrop x + untrop y)

def MinTropical.equivMaxTropical {R : Type u} [LinearOrder R] [Add R] :

MinTropical R ≃+* MaxTropical Rᵒᵈ

The ring structure on MinTropical R is the same as on MaxTropical Rᵒᵈ.

Equations

One or more equations did not get rendered due to their size.

Instances For

def MaxTropical.equivMinTropical {R : Type u} [LinearOrder R] [Add R] :

MaxTropical R ≃+* MinTropical Rᵒᵈ

The ring structure on MaxTropical R is the same as on MinTropical Rᵒᵈ.

Equations

One or more equations did not get rendered due to their size.

Instances For

@[instance_reducible]

instance MinTropical.instOneOfZero {R : Type u} [Zero R] :

One (MinTropical R)

Equations

MinTropical.instOneOfZero = { one := MinTropical.trop 0 }

@[instance_reducible]

instance MaxTropical.instOneOfZero {R : Type u} [Zero R] :

One (MaxTropical R)

Equations

MaxTropical.instOneOfZero = { one := MaxTropical.trop 0 }

@[simp]

theorem MinTropical.trop_zero {R : Type u} [Zero R] :

trop 0 = 1

@[simp]

theorem MaxTropical.trop_zero {R : Type u} [Zero R] :

trop 0 = 1

@[simp]

theorem MinTropical.untrop_one {R : Type u} [Zero R] :

@[simp]

theorem MaxTropical.untrop_one {R : Type u} [Zero R] :

@[instance_reducible]

instance MinTropical.instAddMonoidWithOneOfOrderTopOfZero {R : Type u} [LinearOrder R] [OrderTop R] [Zero R] :

AddMonoidWithOne (MinTropical R)

Equations

One or more equations did not get rendered due to their size.

@[instance_reducible]

instance MaxTropical.instAddMonoidWithOneOfOrderBotOfZero {R : Type u} [LinearOrder R] [OrderBot R] [Zero R] :

AddMonoidWithOne (MaxTropical R)

Equations

One or more equations did not get rendered due to their size.

instance MinTropical.instNontrivialWithTopOfZero {R : Type u} [Zero R] :

Nontrivial (MinTropical (WithTop R))

instance MaxTropical.instNontrivialWithBotOfZero {R : Type u} [Zero R] :

Nontrivial (MaxTropical (WithBot R))

@[instance_reducible]

instance MinTropical.instInvOfNeg {R : Type u} [Neg R] :

Inv (MinTropical R)

Equations

MinTropical.instInvOfNeg = { inv := fun (x : MinTropical R) => MinTropical.trop (-MinTropical.untrop x) }

@[instance_reducible]

instance MaxTropical.instInvOfNeg {R : Type u} [Neg R] :

Inv (MaxTropical R)

Equations

MaxTropical.instInvOfNeg = { inv := fun (x : MaxTropical R) => MaxTropical.trop (-MaxTropical.untrop x) }

@[simp]

theorem MinTropical.untrop_inv {R : Type u} [Neg R] (x : MinTropical R) :

untrop x⁻¹ = -untrop x

@[simp]

theorem MaxTropical.untrop_inv {R : Type u} [Neg R] (x : MaxTropical R) :

untrop x⁻¹ = -untrop x

@[instance_reducible]

instance MinTropical.instDivOfSub {R : Type u} [Sub R] :

Div (MinTropical R)

Equations

MinTropical.instDivOfSub = { div := fun (x y : MinTropical R) => MinTropical.trop (MinTropical.untrop x - MinTropical.untrop y) }

@[instance_reducible]

instance MaxTropical.instDivOfSub {R : Type u} [Sub R] :

Div (MaxTropical R)

Equations

MaxTropical.instDivOfSub = { div := fun (x y : MaxTropical R) => MaxTropical.trop (MaxTropical.untrop x - MaxTropical.untrop y) }

@[simp]

theorem MinTropical.untrop_div {R : Type u} [Sub R] (x y : MinTropical R) :

untrop (x / y) = untrop x - untrop y

@[simp]

theorem MaxTropical.untrop_div {R : Type u} [Sub R] (x y : MaxTropical R) :

untrop (x / y) = untrop x - untrop y

@[instance_reducible]

instance MinTropical.instSemigroupOfAddSemigroup {R : Type u} [AddSemigroup R] :

Semigroup (MinTropical R)

Equations

MinTropical.instSemigroupOfAddSemigroup = { toMul := MinTropical.instMulOfAdd, mul_assoc := ⋯ }

@[instance_reducible]

instance MaxTropical.instSemigroupOfAddSemigroup {R : Type u} [AddSemigroup R] :

Semigroup (MaxTropical R)

Equations

MaxTropical.instSemigroupOfAddSemigroup = { toMul := MaxTropical.instMulOfAdd, mul_assoc := ⋯ }

@[instance_reducible]

instance MinTropical.instCommSemigroupOfAddCommSemigroup {R : Type u} [AddCommSemigroup R] :

CommSemigroup (MinTropical R)

Equations

MinTropical.instCommSemigroupOfAddCommSemigroup = { toSemigroup := MinTropical.instSemigroupOfAddSemigroup, mul_comm := ⋯ }

@[instance_reducible]

instance MaxTropical.instCommSemigroupOfAddCommSemigroup {R : Type u} [AddCommSemigroup R] :

CommSemigroup (MaxTropical R)

Equations

MaxTropical.instCommSemigroupOfAddCommSemigroup = { toSemigroup := MaxTropical.instSemigroupOfAddSemigroup, mul_comm := ⋯ }

@[instance_reducible]

instance MinTropical.instPowOfSMul {R : Type u} {α : Type u_1} [SMul α R] :

Pow (MinTropical R) α

Equations

MinTropical.instPowOfSMul = { pow := fun (x : MinTropical R) (n : α) => MinTropical.trop (n • MinTropical.untrop x) }

@[instance_reducible]

instance MaxTropical.instPowOfSMul {R : Type u} {α : Type u_1} [SMul α R] :

Pow (MaxTropical R) α

Equations

MaxTropical.instPowOfSMul = { pow := fun (x : MaxTropical R) (n : α) => MaxTropical.trop (n • MaxTropical.untrop x) }

@[simp]

theorem MinTropical.untrop_pow {R : Type u} {α : Type u_1} [SMul α R] (x : MinTropical R) (n : α) :

untrop (x ^ n) = n • untrop x

@[simp]

theorem MaxTropical.untrop_pow {R : Type u} {α : Type u_1} [SMul α R] (x : MaxTropical R) (n : α) :

untrop (x ^ n) = n • untrop x

@[simp]

theorem MinTropical.trop_smul {R : Type u} {α : Type u_1} [SMul α R] (x : R) (n : α) :

trop (n • x) = trop x ^ n

@[simp]

theorem MaxTropical.trop_smul {R : Type u} {α : Type u_1} [SMul α R] (x : R) (n : α) :

trop (n • x) = trop x ^ n

@[instance_reducible]

instance MinTropical.instMulOneClassOfAddZeroClass {R : Type u} [AddZeroClass R] :

MulOneClass (MinTropical R)

Equations

MinTropical.instMulOneClassOfAddZeroClass = { toOne := MinTropical.instOneOfZero, toMul := MinTropical.instMulOfAdd, one_mul := ⋯, mul_one := ⋯ }

@[instance_reducible]

instance MaxTropical.instMulOneClassOfAddZeroClass {R : Type u} [AddZeroClass R] :

MulOneClass (MaxTropical R)

Equations

MaxTropical.instMulOneClassOfAddZeroClass = { toOne := MaxTropical.instOneOfZero, toMul := MaxTropical.instMulOfAdd, one_mul := ⋯, mul_one := ⋯ }

@[instance_reducible]

instance MinTropical.instMonoidOfAddMonoid {R : Type u} [AddMonoid R] :

Monoid (MinTropical R)

Equations

One or more equations did not get rendered due to their size.

@[instance_reducible]

instance MaxTropical.instMonoidOfAddMonoid {R : Type u} [AddMonoid R] :

Monoid (MaxTropical R)

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem MinTropical.trop_nsmul {R : Type u} [AddMonoid R] (x : R) (n : ℕ) :

trop (n • x) = trop x ^ n

@[simp]

theorem MaxTropical.trop_nsmul {R : Type u} [AddMonoid R] (x : R) (n : ℕ) :

trop (n • x) = trop x ^ n

@[instance_reducible]

instance MinTropical.instCommMonoidOfAddCommMonoid {R : Type u} [AddCommMonoid R] :

CommMonoid (MinTropical R)

Equations

MinTropical.instCommMonoidOfAddCommMonoid = { toMonoid := MinTropical.instMonoidOfAddMonoid, mul_comm := ⋯ }

@[instance_reducible]

instance MaxTropical.instCommMonoidOfAddCommMonoid {R : Type u} [AddCommMonoid R] :

CommMonoid (MaxTropical R)

Equations

MaxTropical.instCommMonoidOfAddCommMonoid = { toMonoid := MaxTropical.instMonoidOfAddMonoid, mul_comm := ⋯ }

@[instance_reducible]

instance MinTropical.instGroupOfAddGroup {R : Type u} [AddGroup R] :

Group (MinTropical R)

Equations

One or more equations did not get rendered due to their size.

@[instance_reducible]

instance MaxTropical.instGroupOfAddGroup {R : Type u} [AddGroup R] :

Group (MaxTropical R)

Equations

One or more equations did not get rendered due to their size.

@[instance_reducible]

instance MinTropical.instCommGroupOfAddCommGroup {R : Type u} [AddCommGroup R] :

CommGroup (MinTropical R)

Equations

MinTropical.instCommGroupOfAddCommGroup = { toGroup := MinTropical.instGroupOfAddGroup, mul_comm := ⋯ }

@[instance_reducible]

instance MaxTropical.instCommGroupOfAddCommGroup {R : Type u} [AddCommGroup R] :

CommGroup (MaxTropical R)

Equations

MaxTropical.instCommGroupOfAddCommGroup = { toGroup := MaxTropical.instGroupOfAddGroup, mul_comm := ⋯ }

@[simp]

theorem MinTropical.untrop_zpow {R : Type u} [AddGroup R] (x : MinTropical R) (n : ℤ) :

untrop (x ^ n) = n • untrop x

@[simp]

theorem MaxTropical.untrop_zpow {R : Type u} [AddGroup R] (x : MaxTropical R) (n : ℤ) :

untrop (x ^ n) = n • untrop x

@[simp]

theorem MinTropical.trop_zsmul {R : Type u} [AddGroup R] (x : R) (n : ℤ) :

trop (n • x) = trop x ^ n

@[simp]

theorem MaxTropical.trop_zsmul {R : Type u} [AddGroup R] (x : R) (n : ℤ) :

trop (n • x) = trop x ^ n

instance MinTropical.mulLeftMono {R : Type u} [LE R] [Add R] [AddLeftMono R] :

MulLeftMono (MinTropical R)

instance MinTropical.mulRightMono {R : Type u} [LE R] [Add R] [AddRightMono R] :

MulRightMono (MinTropical R)

instance MinTropical.addLeftMono {R : Type u} [LinearOrder R] :

AddLeftMono (MinTropical R)

instance MinTropical.mulLeftStrictMono {R : Type u} [LT R] [Add R] [AddLeftStrictMono R] :

MulLeftStrictMono (MinTropical R)

instance MinTropical.mulRightStrictMono {R : Type u} [Preorder R] [Add R] [AddRightStrictMono R] :

MulRightStrictMono (MinTropical R)

instance MaxTropical.mulLeftMono {R : Type u} [LE R] [Add R] [AddLeftMono R] :

MulLeftMono (MaxTropical R)

instance MaxTropical.mulRightMono {R : Type u} [LE R] [Add R] [AddRightMono R] :

MulRightMono (MaxTropical R)

instance MaxTropical.addLeftMono {R : Type u} [LinearOrder R] :

AddLeftMono (MaxTropical R)

instance MaxTropical.mulLeftStrictMono {R : Type u} [LT R] [Add R] [AddLeftStrictMono R] :

MulLeftStrictMono (MaxTropical R)

instance MaxTropical.mulRightStrictMono {R : Type u} [Preorder R] [Add R] [AddRightStrictMono R] :

MulRightStrictMono (MaxTropical R)

@[instance_reducible]

instance MinTropical.instDistribOfAddLeftMonoOfAddRightMono {R : Type u} [LinearOrder R] [Add R] [AddLeftMono R] [AddRightMono R] :

Distrib (MinTropical R)

Equations

MinTropical.instDistribOfAddLeftMonoOfAddRightMono = { toMul := MinTropical.instMulOfAdd, toAdd := MinTropical.instAdd, left_distrib := ⋯, right_distrib := ⋯ }

@[instance_reducible]

instance MaxTropical.instDistribOfAddLeftMonoOfAddRightMono {R : Type u} [LinearOrder R] [Add R] [AddLeftMono R] [AddRightMono R] :

Distrib (MaxTropical R)

Equations

MaxTropical.instDistribOfAddLeftMonoOfAddRightMono = { toMul := MaxTropical.instMulOfAdd, toAdd := MaxTropical.instAdd, left_distrib := ⋯, right_distrib := ⋯ }

@[simp]

theorem MinTropical.add_pow {R : Type u} [LinearOrder R] [AddMonoid R] [AddLeftMono R] [AddRightMono R] (x y : MinTropical R) (n : ℕ) :

(x + y) ^ n = x ^ n + y ^ n

@[simp]

theorem MaxTropical.add_pow {R : Type u} [LinearOrder R] [AddMonoid R] [AddLeftMono R] [AddRightMono R] (x y : MaxTropical R) (n : ℕ) :

(x + y) ^ n = x ^ n + y ^ n

@[instance_reducible]

instance MinTropical.instCommSemiring {R : Type u} [LinearOrderedAddCommMonoidWithTop R] :

CommSemiring (MinTropical R)

Equations

One or more equations did not get rendered due to their size.

@[simp]

theorem MinTropical.succ_nsmul {R : Type u_1} [LinearOrder R] [OrderTop R] (x : MinTropical R) (n : ℕ) :

(n + 1) • x = x

theorem MinTropical.mul_eq_zero_iff {R : Type u_1} [AddCommMonoid R] {a b : MinTropical (WithTop R)} :

a * b = 0 ↔ a = 0 ∨ b = 0

instance MinTropical.instNoZeroDivisorsWithTop {R : Type u_1} [AddCommMonoid R] :

NoZeroDivisors (MinTropical (WithTop R))