English
A topological ring is J-adic iff powers of J form a basis of open neighborhoods of zero; equivalently, every neighborhood of zero contains some J^n and each J^n is open.
Русский
Топологическое кольцо является J-адическим тогда и только тогда, когда степени J образуют базис открытых окрестностей нуля; эквивалентно тому, что каждая окрестность нуля содержит некоторую J^n и каждый J^n открыт.
LaTeX
$$$IsAdic J\\;\\iff\\; (\\forall n, IsOpen((J^n : \\text{Ideal } R))) \\land (\\forall s\\in 𝓝(0), \\exists n, (J^n : \\text{Set})\\subseteq s)$$$
Lean4
/-- Given a topology on a ring `R` and an ideal `J`, `IsAdic J` means the topology is the
`J`-adic one. -/
def IsAdic [H : TopologicalSpace R] (J : Ideal R) : Prop :=
H = J.adicTopology
