CompletedGroupAlgebra/OpenFiniteQuotientTopology.lean

1import CompletedGroupAlgebra.OpenFiniteQuotientTopology.CanonicalMaps

2import CompletedGroupAlgebra.OpenFiniteQuotientTopology.FiniteQuotients

3import CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteQuotients

4import CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.CanonicalMap

5import CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteComparison

7/-

8PUBLIC_PAGE_SNAPSHOT

9generated_at: 2026-05-27T09:47:29+09:00

10lean_source: lean4/CompletedGroupAlgebra/OpenFiniteQuotientTopology.lean

11translation_root: data/translation

12purpose: identifies the local data snapshot used to build pages/

13placement: after imports, never before imports

15/-!

16# Kernel-neighborhood topology on completed group algebras

18This namespace collects the kernel-neighborhood topology generated by open coefficient ideals and

19open finite group quotients, together with the corresponding inverse-limit model and comparison

20maps for RZ Lemma 5.3.5(a).