Yamaguchi Lean 4 Library
FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower
FoxDifferential/Completed/CoefficientRings/AugmentationIdealPrimePower

FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower

6 sections | 6 files | 86 declarations

Fox Differential / Completed / Coefficient Rings / Prime-Power Augmentation Ideal.

Additive

1 files | 16 declarations | 6 Theorem | 10 Instance
Fox Differential / Completed / Coefficient Rings / Prime-Power Augmentation Ideal / Additive.

Augmentation

1 files | 22 declarations | 15 Theorem | 6 Definition | 1 Abbreviation
Fox Differential / Completed / Coefficient Rings / Prime-Power Augmentation Ideal / Augmentation.

LimitEquiv

1 files | 16 declarations | 13 Theorem | 3 Definition
Fox Differential / Completed / Coefficient Rings / Prime-Power Augmentation Ideal / Limit Equivalence.

Module

1 files | 7 declarations | 2 Theorem | 5 Instance
Fox Differential / Completed / Coefficient Rings / Prime-Power Augmentation Ideal / Module.

Stage

1 files | 12 declarations | 4 Theorem | 4 Definition | 3 Abbreviation | 1 Instance
Fox Differential / Completed / Coefficient Rings / Prime-Power Augmentation Ideal / Stage.

SubtypeLinear

1 files | 13 declarations | 9 Theorem | 4 Definition
Fox Differential / Completed / Coefficient Rings / Prime-Power Augmentation Ideal / Subtype Linear.