decidableLT

Mathlib.Algebra.Tropical.Basic

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

Lean4

instance decidableLT [LT R] [DecidableLT R] : DecidableLT (Tropical R) := fun x y =>
  ‹DecidableLT R› (untrop x) (untrop y)

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

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

Разделы

Аффилиация

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