instNoZeroDivisorsWithTop

Mathlib.Algebra.Tropical.Basic

URI: https://scilib.ai/kg/mathlib#Tropical.instNoZeroDivisorsWithTop

English

For Tropical R with linear order and top element, for every x and n, (n+1)·x = x.

Русский

Для Tropical R с линейным порядком и верхом, для любого x и n выполняется (n+1)·x = x.

LaTeX

$$$\forall x \in \mathrm{Tropical}(R),\forall n \in \mathbb{N}, (n+1) \cdot x = x$$$

Lean4

instance {R : Type*} [AddCommMonoid R] : NoZeroDivisors (Tropical (WithTop R)) :=
  ⟨mul_eq_zero_iff.mp⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru