add_left_cancel_iff

Mathlib.Data.Nat.PartENat

URI: https://scilib.ai/kg/mathlib#PartENat.add_left_cancel_iff

← MathLib Explorer

English

If a ≠ ⊤, then a + b = a + c iff b = c.

Русский

Если a ≠ ⊤, то a + b = a + c эквивалентно b = c.

LaTeX

$$$\\forall {a\\, b\\, c : \\mathrm{PartENat}},\\; a \\neq \\top \\Rightarrow (a + b = a + c \\iff b = c)$$$

Lean4

protected theorem add_left_cancel_iff {a b c : PartENat} (ha : a ≠ ⊤) : a + b = a + c ↔ b = c := by
  rw [add_comm a, add_comm a, PartENat.add_right_cancel_iff ha]

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

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

Разделы

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

Аффилиация

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