zero_add

Mathlib.SetTheory.Nimber.Basic

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

English

For any nimber a, 0 + a = a.

Русский

Для любого нимбера a, 0 + a = a.

LaTeX

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

Lean4

protected theorem zero_add (a : Nimber) : 0 + a = a := by rw [Nimber.add_comm, Nimber.add_zero]

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

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

Разделы

Аффилиация

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