isNilpotent_of_subsingleton — Mathlib

English

In a subsingleton algebra with zero and powers, every element is nilpotent.

Русский

В тождественно-единственном алгебраическом структуре с нулём и показателями, каждый элемент нилпотентен.

LaTeX

$$$\\forall x:\\,R,\\IsNilpotent(x)$$$

Lean4

@[simp]
theorem isNilpotent_of_subsingleton [Zero R] [Pow R ℕ] [Subsingleton R] : IsNilpotent x :=
  ⟨0, Subsingleton.elim _ _⟩

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