topologicalNilradical — Mathlib

English

The topological nilradical of a ring with a linear topology is the set of all topologically nilpotent elements, forming an ideal.

Русский

Топологический нильрадикал кольца с линейной топологией есть множество элементов, являющихся топологически нильпотентными, образующее идеал.

LaTeX

$$$\text{topologicalNilradical}(R) = \{a \in R : \text{IsTopologicallyNilpotent}(a)\}.$$$

Lean4

/-- The topological nilradical of a ring with a linear topology -/
@[simps]
def _root_.topologicalNilradical : Ideal R
    where
  carrier := {a | IsTopologicallyNilpotent a}
  add_mem' := add
  zero_mem' := zero
  smul_mem' := mul_left

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