FoxDifferential/Completed.lean

1import FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Additive

2import FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Augmentation

3import FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.LimitEquiv

4import FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Module

5import FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Stage

6import FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.SubtypeLinear

7import CompletedGroupAlgebra.Basic.AllFinite.Stage

8import CompletedGroupAlgebra.OpenFiniteQuotientTopology.CanonicalMaps

9import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebra

10import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.Augmentation

11import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.AugmentationIdeal

12import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.CoeffMap

13import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.AddCommGroup

14import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.Augmentation

15import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.CompletionMap

16import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Augmentation

17import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.Augmentation

18import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.InClass.StageCoeffMap

19import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.StageCoeffMap.AllFinite

20import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.StageCoeffMap.Coeff

21import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.AddCommGroup

22import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Projection

23import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Ring

24import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.System

25import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.Augmentation

26import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.Map

27import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Basic

28import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.AddCommGroup

29import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.GroupLike

30import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Multiplicative

31import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass.System.Ring.Projection

32import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Module

33import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Basic

34import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.AddCommGroup

35import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.GroupLike

36import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.Multiplicative

37import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.Projection

38import FoxDifferential.Completed.Comparison.DiscreteCompletion

39import FoxDifferential.Completed.Comparison.FiniteStage

40import FoxDifferential.Completed.Comparison.QuotientFamily

41import FoxDifferential.Completed.Comparison.SourceProjection

42import FoxDifferential.Completed.DifferentialModule.Identity

43import FoxDifferential.Completed.DifferentialModule.Map.Comap

44import FoxDifferential.Completed.DifferentialModule.Map.GroupLike

45import FoxDifferential.Completed.DifferentialModule.Map.Limit

46import FoxDifferential.Completed.DifferentialModule.Map.Stage

47import FoxDifferential.Completed.DifferentialModule.Map.Surjective

48import FoxDifferential.Completed.DifferentialModule.TargetQuotient.Basic

49import FoxDifferential.Completed.DifferentialModule.TargetQuotient.Fundamental

50import FoxDifferential.Completed.DifferentialModule.TargetQuotient.MulProjection

51import FoxDifferential.Completed.DifferentialModule.TargetQuotient.StageMap

52import FoxDifferential.Completed.DifferentialModule.TargetQuotient.Surjective

53import FoxDifferential.Completed.Continuous.Automorphism

54import FoxDifferential.Completed.Continuous.Free.DiscreteGenerators

55import FoxDifferential.Completed.Continuous.Free.Rules

56import FoxDifferential.Completed.Continuous.Topology

57import FoxDifferential.Completed.Continuous.ChainRule.Basic

58import FoxDifferential.Completed.Continuous.ChainRule.Iterated

59import FoxDifferential.Common.Jacobian

60import FoxDifferential.Completed.Continuous.Naturality

61import FoxDifferential.Completed.Continuous.TailExactness

62import FoxDifferential.Completed.Continuous.TopologicalGeneration

63import FoxDifferential.Completed.Continuous.Universal.Basic

64import FoxDifferential.Completed.Continuous.Universal.FiniteStage

65import FoxDifferential.Completed.Continuous.Universal.NaturalTopology

66import FoxDifferential.Completed.Continuous.Universal.System

67import FoxDifferential.Completed.Continuous.SemidirectKernelBasis

68import FoxDifferential.Completed.FiniteStage.Basic

69import FoxDifferential.Completed.FiniteStage.BoundaryCycles

70import FoxDifferential.Completed.FiniteStage.BoundaryCycleHom

71import FoxDifferential.Completed.FiniteStage.RelationModule

72import FoxDifferential.Completed.FiniteStage.RelationAction

73import FoxDifferential.Completed.FiniteStage.RelationSubmodule

74import FoxDifferential.Completed.FiniteStage.BoundaryQuotient

75import FoxDifferential.Completed.FiniteStage.SemidirectCycles

76import FoxDifferential.Completed.FiniteStage.BoundarySubgroups

77import FoxDifferential.Completed.FiniteStage.RelationRealization

78import FoxDifferential.Completed.FiniteStage.RelationIdeal

79import FoxDifferential.Completed.FiniteStage.SourceBoundary

80import FoxDifferential.Completed.FiniteStage.RelationIdealDerivative

81import FoxDifferential.Completed.FiniteStage.CoeffMap.Augmentation

82import FoxDifferential.Completed.FiniteStage.CoeffMap.Semidirect

83import FoxDifferential.Completed.FiniteStage.CoeffMap.Boundary

84import FoxDifferential.Completed.FiniteStage.CoeffMap.BoundaryCycles

85import FoxDifferential.Completed.FiniteStage.MagnusQuotient

86import FoxDifferential.Completed.FiniteStage.PrimePower.Completion.Source.Index

87import FoxDifferential.Completed.FiniteStage.PrimePower.Completion.Source.LimitMap

88import FoxDifferential.Completed.FiniteStage.PrimePower.Completion.Source.Representatives

89import FoxDifferential.Completed.FiniteStage.PrimePower.Completion.Target

90import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.CompletedSource

91import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.CompletedTarget

92import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Limit

93import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Vector

94import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.OnGroup.Vector

95import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.OnGroup.Projection

96import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Source.Fundamental

97import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Source.GroupLike

98import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Source.Mul

99import FoxDifferential.Completed.FiniteStage.PrimePower.Derivative.Source.SpecialValues

100import FoxDifferential.Completed.FiniteStage.PrimePower.System.Basic

101import FoxDifferential.Completed.FiniteStage.PrimePower.System.Semidirect

102import FoxDifferential.Completed.FiniteStage.PrimePower.System.Limit.AddCommGroup

103import FoxDifferential.Completed.FiniteStage.PrimePower.System.Limit.CoeffMap

104import FoxDifferential.Completed.FiniteStage.PrimePower.System.Limit.Mul

105import FoxDifferential.Completed.FiniteStage.PrimePower.System.Limit.Semidirect

106import FoxDifferential.Completed.FiniteStage.Stage.Derivative.Boundary

107import FoxDifferential.Completed.FiniteStage.Stage.Derivative.Relators

108import FoxDifferential.Completed.FiniteStage.Stage.Derivative.Rules

109import FoxDifferential.Completed.FiniteStage.Stage.Derivative.Quotient.Fundamental

110import FoxDifferential.Completed.FiniteStage.Stage.Fundamental.Formula

111import FoxDifferential.Completed.FiniteStage.Stage.KernelIdeal

112import FoxDifferential.Completed.FiniteStage.Stage.Naturality

113import FoxDifferential.Completed.FiniteStage.Stage.Semidirect

114import FoxDifferential.Completed.FiniteStage.Stage.Source

115import FoxDifferential.Completed.FiniteStage.TargetMap

116import FoxDifferential.Completed.FiniteStage.Bifiltered.Transition

117import FoxDifferential.Completed.FiniteStage.Bifiltered.System

118import FoxDifferential.Completed.FiniteStage.Bifiltered.InverseSystem

119import FoxDifferential.Completed.FreeProC.SemidirectLift

120import FoxDifferential.Completed.FreeProC.Uniqueness.Derivative

121import FoxDifferential.Completed.FreeProC.Uniqueness.Existence

122import FoxDifferential.Completed.FreeProC.Uniqueness.Lift

123import FoxDifferential.Completed.FreeProC.Uniqueness.Morphism

124import FoxDifferential.Completed.FreeProC.Uniqueness.SemidirectHom

125import FoxDifferential.Completed.FreeProC.Density

126import FoxDifferential.Completed.FreeProC.StageApproximation

127import FoxDifferential.Completed.FreeProC.RelationSubmoduleApproximation

128import FoxDifferential.Completed.FreeProC.StageProjection

129import FoxDifferential.Completed.FreeProC.QuotientKernelBasis

130import FoxDifferential.Completed.FreeProC.CofinalQuotientKernelBasis

131import FoxDifferential.Completed.FreeProC.PrimePowerStageProjection

132import FoxDifferential.Completed.FreeProC.BifilteredStageProjection

133import FoxDifferential.Completed.FreeProC.BifilteredSystemStageProjection

134import FoxDifferential.Completed.FreeProC.CoordinateStageProjection

135import FoxDifferential.Completed.FreeProC.BifilteredCoefficientStageProjection

136import FoxDifferential.Completed.FreeProC.ProCIntegerStageCoeffProjection

137import FoxDifferential.Completed.FreeProC.ProCIntegerBifilteredStageProjection

138import FoxDifferential.Completed.FreeProC.ProCIntegerBifilteredStageRightProjection

139import FoxDifferential.Completed.FreeProC.FiniteQuotientStages

140import FoxDifferential.Completed.FreeProC.SemidirectKernelBasis

141import FoxDifferential.Completed.Residue.Core

142import FoxDifferential.Completed.Residue.FreeGroup.Basic

143import FoxDifferential.Completed.Residue.FreeGroup.Boundary

144import FoxDifferential.Completed.Residue.FreeGroup.Coordinates

145import FoxDifferential.Completed.Residue.FreeGroup.Fundamental

146import FoxDifferential.Completed.Residue.FreeGroup.Universal

147import FoxDifferential.Completed.Semidirect

148import FoxDifferential.Completed.ProCIntegerCoefficients.Augmentation

149import FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Closure

150import FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.FiniteStage

151import FoxDifferential.Completed.ProCIntegerCoefficients.AugmentationIdeal.Kernel

152import FoxDifferential.Completed.ProCIntegerCoefficients.Core

153import FoxDifferential.Completed.ProCIntegerCoefficients.FreeGroup.Fundamental

154import FoxDifferential.Completed.ProCIntegerCoefficients.Naturality

155

156/-

157PUBLIC_PAGE_SNAPSHOT

158generated_at: 2026-05-27T09:47:29+09:00

159lean_source: lean4/FoxDifferential/Completed.lean

160translation_root: data/translation

161purpose: identifies the local data snapshot used to build pages/

162placement: after imports, never before imports

163-/

164/-!

165# Completed Fox calculus

166

167This entry point collects completed/profinite Fox-differential theory: completed coefficient rings, completed differential modules, continuous crossed differentials, finite-stage comparison, free pro-\(C\) formulas, and semidirect constructions.

168-/