Yamaguchi Lean 4 Library
CompletedGroupAlgebra.ProfiniteModules
CompletedGroupAlgebra/ProfiniteModules

CompletedGroupAlgebra.ProfiniteModules

2 sections | 13 files | 170 declarations

This module develops completed group algebras through finite quotient stages, transition maps, coefficient change, augmentation, comparison maps, and inverse-limit topology.

Basic

6 files | 70 declarations | 50 Theorem | 18 Definition | 1 Abbreviation | 1 Structure
A compact Hausdorff totally disconnected topological ring.

FiniteGroupAlgebra

7 files | 100 declarations | 77 Theorem | 22 Definition | 1 Structure
Wrapper for the `CompletedGroupAlgebra.ProfiniteModules.FiniteGroupAlgebra.Augmentation` folder.