mem_topologicalNilradical_iff — Mathlib

English

For any element a, a is in the topological nilradical iff a is topologically nilpotent.

Русский

Для любого элемента a верно: a принадлежит топологическому нильрадикалу тогда и только тогда, когда a топологически нильпотентен.

LaTeX

$$$a \in \operatorname{topologicalNilradical}(R) \iff \text{IsTopologicallyNilpotent}(a).$$$

Lean4

theorem mem_topologicalNilradical_iff {a : R} : a ∈ topologicalNilradical R ↔ IsTopologicallyNilpotent a := by
  simp [topologicalNilradical]

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