isAddUnit_iff

Mathlib.Algebra.Group.Nat.Units

URI: https://scilib.ai/kg/mathlib#Nat.isAddUnit_iff

English

Let n be a natural number. Then n is an additive unit if and only if n = 0.

Русский

Пусть n ∈ ℕ. Тогда n является единицей сложения тогда и только тогда, когда n = 0.

LaTeX

$$$ \forall n \in \mathbb{N}, \; \mathrm{IsAddUnit}(n) \iff n = 0 $$$

Lean4

/-- Alias of `isAddUnit_iff_eq_zero` for discoverability. -/
protected theorem isAddUnit_iff {n : ℕ} : IsAddUnit n ↔ n = 0 :=
  isAddUnit_iff_eq_zero

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

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

Разделы

Аффилиация

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