Theorems · Theorem · commutative algebra

isAdic_iff

∀ {R : Type u_1} [inst : CommRing R] [top : TopologicalSpace R] [IsTopologicalRing R] {J : Ideal R},
  IsAdic J ↔ (∀ (n : ℕ), IsOpen ↑(J ^ n)) ∧ ∀ s ∈ nhds 0, ∃ n, ↑(J ^ n) ⊆ s

A topological ring is J-adic if and only if it admits the powers of J as a basis of open neighborhoods of zero.

Defined in

Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology

Cited by

2 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingTopologicalSpaceIsTopologicalRing