add_left_cancel

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

English

Same as Add_left_inj with a different formulation; preserved for completeness.

Русский

То же самое, что Add_left_inj, другая формулировка.

LaTeX

$$Same content as Add_left_inj$$

Lean4

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

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

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

Разделы

Аффилиация

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