right_eq_zero_of_add_eq_zero

Mathlib.SetTheory.Ordinal.Arithmetic

URI: https://scilib.ai/kg/mathlib#Ordinal.right_eq_zero_of_add_eq_zero

English

From a + b = 0 it follows that b = 0.

Русский

Из a + b = 0 следует, что b = 0.

LaTeX

$$$\forall a,b \in \mathrm{Ordinal},\ a+b=0 \Rightarrow b=0$$$

Lean4

theorem right_eq_zero_of_add_eq_zero {a b : Ordinal} (h : a + b = 0) : b = 0 :=
  (add_eq_zero_iff.1 h).2

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

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

Разделы

Аффилиация

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