instIsOrderedAddMonoid

Mathlib.Algebra.Order.Ring.Rat

URI: https://scilib.ai/kg/mathlib#Rat.instIsOrderedAddMonoid

English

ℚ is an ordered additive monoid; addition is compatible with the order.

Русский

Числа λка ℚ образуют упорядоченный аддитивный моноид; сложение совместимо с порядком.

LaTeX

$$IsOrderedAddMonoid(\\mathbb{Q})$$

Lean4

instance instIsOrderedAddMonoid : IsOrderedAddMonoid ℚ where add_le_add_left := fun _ _ ab _ => Rat.add_le_add_left.2 ab

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

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

Разделы

Аффилиация

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