FoxDifferential/Completed/FiniteStage/PrimePower.lean

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

23PUBLIC_PAGE_SNAPSHOT

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

25lean_source: lean4/FoxDifferential/Completed/FiniteStage/PrimePower.lean

26translation_root: data/translation

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

28placement: after imports, never before imports

30/-!

31# FoxDifferential.Completed.FiniteStage.PrimePower

33Wrapper for the `FoxDifferential.Completed.FiniteStage.PrimePower` folder.