Yamaguchi Lean 4 Library
FoxDifferential.Completed
FoxDifferential/Completed

FoxDifferential.Completed

9 sections | 217 files | 2382 declarations

This module formalizes completed Fox coordinates for profinite groups.

CoefficientRings

52 files | 437 declarations | 245 Theorem | 67 Definition | 30 Abbreviation | 95 Instance
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.

Comparison

5 files | 66 declarations | 59 Theorem | 2 Definition | 4 Abbreviation | 1 Structure
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.

Continuous

22 files | 626 declarations | 452 Theorem | 119 Definition | 14 Abbreviation | 1 Structure | 40 Instance
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.

DifferentialModule

14 files | 44 declarations | 31 Theorem | 13 Definition
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.

FiniteStage

78 files | 567 declarations | 408 Theorem | 115 Definition | 15 Abbreviation | 1 Structure | 28 Instance
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.

FreeProC

24 files | 296 declarations | 237 Theorem | 57 Definition | 2 Instance
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.

ProCIntegerCoefficients

13 files | 268 declarations | 188 Theorem | 56 Definition | 10 Abbreviation | 14 Instance
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.

Residue

8 files | 48 declarations | 31 Theorem | 14 Definition | 3 Abbreviation
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.

Semidirect

1 files | 30 declarations | 22 Theorem | 3 Definition | 1 Structure | 4 Instance
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.