instNontrivialWithTopOfZero

Mathlib.Algebra.Tropical.Basic

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

English

If R has a zero, Tropical(WithTop R) is a nontrivial type (there exist distinct elements).

Русский

Если R содержит ноль, Tropical(WithTop R) ненулевой тип (существуют различные элементы).

LaTeX

$$$\\exists a,b \\in Tropical(WithTop R), a \\neq b$$$

Lean4

instance [Zero R] : Nontrivial (Tropical (WithTop R)) :=
  ⟨⟨0, 1, trop_injective.ne WithTop.top_ne_coe⟩⟩

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

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

Разделы

Аффилиация

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