English
Let A be a topological ring. The adic topology associated with the zero ideal is exactly the discrete topology on A; conversely, if the adic topology is discrete, then the topology on A is discrete.
Русский
Пусть A — топологическое кольцо. Адическая топология, соответствующая нулевому идеалу, совпадает с дискретной топологией на A; наоборот, если адическая топология дискретна, то топология на A дискретна.
LaTeX
$$$IsAdic(\perp : Ideal A) \iff DiscreteTopology A$$$
Lean4
theorem is_bot_adic_iff {A : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A] :
IsAdic (⊥ : Ideal A) ↔ DiscreteTopology A := by
rw [isAdic_iff]
constructor
· rintro ⟨h, _h'⟩
rw [discreteTopology_iff_isOpen_singleton_zero]
simpa using h 1
· intros
constructor
· simp
· intro U U_nhds
use 1
simp [mem_of_mem_nhds U_nhds]
