addLeftCancelSemigroup

Mathlib.Data.Rat.Defs

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

English

The rationals under addition form a left-cancellative semigroup: if a + b = a + c, then b = c.

Русский

Рациональные числа по сложению образуют левую отмену: если a + b = a + c, то b = c.

LaTeX

$$$\forall a,b,c \in \mathbb{Q},\ a + b = a + c \Rightarrow b = c$$$

Lean4

instance addLeftCancelSemigroup : AddLeftCancelSemigroup ℚ := by infer_instance

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

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

Разделы

Аффилиация

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