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

Source: ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates

1import ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Basic
2import ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Equiv
3import ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Topology
4import ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Comparison
6/-!
7# Closed-generated completed Fox coordinates
9This aggregate collects the construction, equivalences, topology, and comparison formulas for
10closed-generated coordinates in completed Fox differential modules.
11-/