instIsLeftCancelAdd

Mathlib.SetTheory.Nimber.Basic

URI: https://scilib.ai/kg/mathlib#Nimber.instIsLeftCancelAdd

← MathLib Explorer

English

Addition in Nimbers is left-cancellative: if a + x = a + y, then x = y.

Русский

Сложение Nimbers слева карательно: если a + x = a + y, значит x = y.

LaTeX

$$IsLeftCancelAdd Nimber$$

Lean4

instance : IsLeftCancelAdd Nimber := by
  constructor
  intro a b c h
  apply le_antisymm <;> apply le_of_not_gt
  · exact fun hc => (add_ne_of_lt a b).2 c hc h.symm
  · exact fun hb => (add_ne_of_lt a c).2 b hb h

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

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

Разделы

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

Аффилиация

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