zero

Mathlib.Topology.Algebra.TopologicallyNilpotent

URI: https://scilib.ai/kg/mathlib#IsTopologicallyNilpotent.zero

← MathLib Explorer

English

Zero is topologically nilpotent.

Русский

Единица ноль топологически нильпотентна.

LaTeX

$$$\text{IsTopologicallyNilpotent}(0).$$$

Lean4

/-- `0` is topologically nilpotent -/
theorem zero : IsTopologicallyNilpotent (0 : R) :=
  tendsto_atTop_of_eventually_const (i₀ := 1) (fun _ hi => by rw [zero_pow (Nat.ne_zero_iff_zero_lt.mpr hi)])

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

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

Разделы

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

Аффилиация

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