decidableLE

Mathlib.Algebra.Tropical.Basic

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

Lean4

instance decidableLE [LE R] [DecidableLE R] : DecidableLE (Tropical R) := fun x y =>
  ‹DecidableLE R› (untrop x) (untrop y)

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

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

Разделы

Аффилиация

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