instDistribTropical — Mathlib

English

Tropical R forms a distributive algebra: multiplication distributes over addition in the tropical sense.

Русский

Тропическое пространство образует дистрибутивную алгебру: умножение распределяется по сложению в тропическом смысле.

LaTeX

$$$\forall a,b,c \in \mathrm{Tropical}(R),\ a\cdot(b+c) = a\cdot b + a\cdot c \land (a+b)\cdot c = a\cdot c + b\cdot c$$$

Lean4

instance instDistribTropical [LinearOrder R] [Add R] [AddLeftMono R] [AddRightMono R] : Distrib (Tropical R)
    where
  mul := (· * ·)
  add := (· + ·)
  left_distrib _ _ _ := untrop_injective (min_add_add_left _ _ _).symm
  right_distrib _ _ _ := untrop_injective (min_add_add_right _ _ _).symm

Похожие утверждения