addRightCancelSemigroup

Mathlib.Data.Rat.Defs

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

English

The rationals under addition form a right-cancellative semigroup: if x + a = y + a, then x = y.

Русский

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

LaTeX

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

Lean4

instance addRightCancelSemigroup : AddRightCancelSemigroup ℚ := by infer_instance

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

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

Разделы

Аффилиация

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