instAddRightCancelSemigroup

Mathlib.Data.Real.Basic

URI: https://scilib.ai/kg/mathlib#Real.instAddRightCancelSemigroup

English

Addition on the real numbers is right-cancellative: if b + a = c + a then b = c for all a,b,c ∈ ℝ.

Русский

Сложение справа отменяется: если b + a = c + a, то b = c для всех a,b,c ∈ ℝ.

LaTeX

$$$$b+a=c+a \\Rightarrow b=c \\quad (a,b,c \\in \\mathbb{R})$$$$

Lean4

instance : AddRightCancelSemigroup ℝ := by infer_instance

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

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

Разделы

Аффилиация

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