Yamaguchi Lean 4 Library
ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System
ProCGroups/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/System

ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System

3 sections | 3 files | 35 declarations

This aggregate re-exports the following parts of the Fox differential API:

  • Completed.CoefficientRings.CompletedGroupAlgebraModN.System.CompletionMap
import
Imported by

AddCommGroup

1 file | 18 declarations | 10 Theorems | 8 Instances
The principal declarations in this module are: - `instAddCommGroupModNCompletedGroupAlgebraStage` Each finite mod-\(n\) group-algebra stage carries its standard additive commuta...

Basic

1 file | 14 declarations | 7 Theorems | 3 Definitions | 3 Abbreviations | 1 Instance
The principal declarations in this module are: - `ModNCompletedGroupAlgebraStage` The mod-\(N\) completed group-algebra stage combines the finite group quotient with the coeffic...

CompletionMap

1 file | 3 declarations | 2 Theorems | 1 Definition
The principal declarations in this module are: - `toModNCompletedGroupAlgebra` The canonical map \((\mathbb{Z}/n\mathbb{Z})[G] \to \varprojlim_U (\mathbb{Z}/n\mathbb{Z})[G/U]\)....