Yamaguchi Lean 4 Library
Source: ProCGroups.FoxDifferential.Completed
ProCGroups/FoxDifferential/Completed/Source

Source: ProCGroups.FoxDifferential.Completed

1import ProCGroups.FoxDifferential.Completed.CoefficientRings
2import ProCGroups.FoxDifferential.Completed.Comparison
3import ProCGroups.FoxDifferential.Completed.Continuous
4import ProCGroups.FoxDifferential.Completed.DifferentialModule
5import ProCGroups.FoxDifferential.Completed.FiniteStage
6import ProCGroups.FoxDifferential.Completed.FreeProC
7import ProCGroups.FoxDifferential.Completed.ProCIntegerCoefficients
8import ProCGroups.FoxDifferential.Completed.Residue
9import ProCGroups.FoxDifferential.Completed.Semidirect
11/-!
12# Fox Differential / Completed
14This module formalizes completed Fox coordinates for profinite groups.
15-/