zero_ne_trop_coe

Mathlib.Algebra.Tropical.Basic

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

English

0 is not equal to trop(WithTop.some x) in Tropical(WithTop R).

Русский

0 не равно trop(WithTop.some x) в Tropical(WithTop R).

LaTeX

$$$0 \\neq \\operatorname{trop}(\\operatorname{WithTop}.some(x))$$$

Lean4

@[simp]
theorem zero_ne_trop_coe (x : R) : 0 ≠ (trop x : Tropical (WithTop R)) :=
  nofun

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

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

Разделы

Аффилиация

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