adicTopology — Mathlib

English

The adic topology on R determined by an ideal I is the topology generated by the basis {I^n}.

Русский

Адическая топология на кольце R, задаваемая идеалом I, — это топология, порождаемая базисом {I^n}.

LaTeX

$$$\\text{adicTopology}(I) := (\\text{basis of powers of }I).topology$$$

Lean4

/-- The adic topology associated to an ideal `I`. This topology admits powers of `I` as a basis of
neighborhoods of zero. It is compatible with the ring structure and is non-archimedean. -/
def adicTopology (I : Ideal R) : TopologicalSpace R :=
  (adic_basis I).topology

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