All.lean
Nyll.ProCGroups.FoxDifferential.Completed.Continuous.All
0 declarations indexed from sourceView source ↗
Module documentation
Continuous completed Fox calculus
This aggregate imports the topology and continuity of completed Fox coordinates, their naturality and chain rules, free-source and universal constructions, topological-generation formulas, semidirect-kernel bases, automorphism formulas, and the resulting tail exactness theorems. The common algebraic CrossedHom interface is supplied by FoxDifferential.Common; finite-stage and completion-specific implementations are collected here.
Imports12
- Nyll.ProCGroups.FoxDifferential.Completed.Continuous.Automorphism
- Nyll.ProCGroups.FoxDifferential.Completed.Continuous.ChainRule.All
- Nyll.ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.All
- Nyll.ProCGroups.FoxDifferential.Completed.Continuous.Free.All
- Nyll.ProCGroups.FoxDifferential.Completed.Continuous.Magnus.All
- Nyll.ProCGroups.FoxDifferential.Completed.Continuous.Naturality
- Nyll.ProCGroups.FoxDifferential.Completed.Continuous.PresentedCoordinates
- Nyll.ProCGroups.FoxDifferential.Completed.Continuous.SemidirectKernelBasis
- Nyll.ProCGroups.FoxDifferential.Completed.Continuous.TailExactness
- Nyll.ProCGroups.FoxDifferential.Completed.Continuous.TopologicalGeneration
- Nyll.ProCGroups.FoxDifferential.Completed.Continuous.Topology
- Nyll.ProCGroups.FoxDifferential.Completed.Continuous.Universal.All
Imported by1
This module has no indexed declarations. Its imports and full source are available here.