add_right_inj

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

← MathLib Explorer

English

If IsRightCancelAdd holds and z ≠ ⊤, then x + z = y + z iff x = y.

Русский

При условии IsRightCancelAdd и z ≠ ⊤ верно: x + z = y + z эквивалентно x = y.

LaTeX

$$$(IsRightCancelAdd α)\\; (hz:\\ z \\neq \\top) \\Rightarrow x+z = y+z \\iff x = y$$$

Lean4

theorem add_right_inj [IsRightCancelAdd α] (hz : z ≠ ⊤) : x + z = y + z ↔ x = y := by lift z to α using hz;
  cases x <;> cases y <;> simp [← coe_add]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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