zero_nadd

Mathlib.SetTheory.Ordinal.NaturalOps

URI: https://scilib.ai/kg/mathlib#Ordinal.zero_nadd

English

The zero element on the left behaves neutrally: 0 ♯ a = a.

Русский

Левый ноль нейтрален: 0 ♯ a = a.

LaTeX

$$$0 \# a = a$$$

Lean4

@[simp]
theorem zero_nadd : 0 ♯ a = a := by rw [nadd_comm, nadd_zero]

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

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

Разделы

Аффилиация

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