Free Augmentation

Abstract

This module supplies the indicated step in the unbounded solidification construction.

Theorem 1.1 (free Augmentation Section comp).

Lean statement: D5/S3/HomologicalAlgebra/Solid/Supplier/FreeAugmentation.freeAugmentationSection_comp

Proof. Machine-checked in Lean as D5/S3/HomologicalAlgebra/Solid/Supplier/FreeAugmentation.freeAugmentationSection_comp (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact declaration is supplied by the compiled Lean source. This module supplies the indicated step in the unbounded solidification construction.

References

• Truth anchor: D5/S3/HomologicalAlgebra/Solid/Supplier/FreeAugmentation.freeAugmentationSection_comp
• Dependency: D5/S3/HomologicalAlgebra/Solid/DiscreteInt
• Dependency: D5/S3/HomologicalAlgebra/Solid/Early