nadd_nat

Mathlib.SetTheory.Ordinal.NaturalOps

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

← MathLib Explorer

English

For a natural n, a ♯ n = a + n.

Русский

Для натурального n верно: a ♯ n = a + n.

LaTeX

$$$a \# n = a + n$$$

Lean4

@[simp]
theorem nadd_nat (n : ℕ) : a ♯ n = a + n := by
  induction n with
  | zero => simp
  | succ n hn => rw [Nat.cast_succ, add_one_eq_succ, nadd_succ, add_succ, hn]

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

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

Разделы

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

Аффилиация

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