add_left_cancel

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

URI: https://scilib.ai/kg/mathlib#WithBot.add_left_cancel

English

If x ≠ ⊥ and x + y = x + z, then y = z.

Русский

Если x ≠ ⊥ и x + y = x + z, тогда y = z.

LaTeX

$$$ (\\text{hx} : x \\neq \\bot) (h : x + y = x + z) : y = z $$$

Lean4

theorem add_left_cancel [IsLeftCancelAdd α] (hx : x ≠ ⊥) (h : x + y = x + z) : y = z :=
  (WithBot.add_left_inj hx).1 h

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

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

Разделы

Аффилиация

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