Yamaguchi Lean 4 Library
Homepage
Source: ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic
ProCGroups
/
CompletedGroupAlgebra
/
ProfiniteModules
/
Basic
/
Source
Source: ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic
1
import
ProCGroups.CompletedGroupAlgebra.ProfiniteModules.Basic.OpenIdeals
2
3
/-!
4
# Basic theory of profinite modules
5
6
This aggregate exports the bundled definitions of profinite rings and modules, their open
7
submodules and ideals, finite quotient separation, and generating sets converging to zero.
8
-/