add_eq_zero_iff

Mathlib.Data.Nat.WithBot

URI: https://scilib.ai/kg/mathlib#Nat.WithBot.add_eq_zero_iff

← MathLib Explorer

English

For n,m ∈ WithBot ℕ, n + m = 0 if and only if n = 0 and m = 0.

Русский

Для n,m ∈ WithBot ℕ, n + m = 0 тогда и только тогда, когда n = 0 и m = 0.

LaTeX

$$$$ n + m = 0 \\\\Leftrightarrow (n = 0 \\\\land m = 0) $$$$

Lean4

theorem add_eq_zero_iff {n m : WithBot ℕ} : n + m = 0 ↔ n = 0 ∧ m = 0 :=
  by
  cases n
  · simp [WithBot.bot_add]
  cases m
  · simp [WithBot.add_bot]
  simp [← WithBot.coe_add]

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

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

Разделы

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

Аффилиация

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