FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass.lean

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

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

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

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

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

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

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

9/-

10PUBLIC_PAGE_SNAPSHOT

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

12lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/InClass.lean

13translation_root: data/translation

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

15placement: after imports, never before imports

17/-!

18# FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass

20Wrapper for the `FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.InClass` folder.