add_comm

Mathlib.SetTheory.Nimber.Basic

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

← MathLib Explorer

English

Nimber addition is commutative: a + b = b + a.

Русский

Сложение Nimbers коммутативно: a + b = b + a.

LaTeX

$$$\\\\forall a\\\\ b: \\\\mathrm{Nimber},\\\\ a + b = b + a.$$$

Lean4

protected theorem add_comm (a b : Nimber) : a + b = b + a :=
  by
  rw [add_def, add_def]
  simp_rw [or_comm]
  congr! 7 <;> (rw [and_congr_right_iff]; intro; rw [Nimber.add_comm])
termination_by (a, b)

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

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

Разделы

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

Аффилиация

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