Exact Derived Homology Natural

Abstract

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

Theorem 1.1 (exact Derived Homology Nat Iso hom app Q).

Lean statement: D5/S3/HomologicalAlgebra/Solid/ExactDerivedHomologyNatural.exactDerivedHomologyNatIso_hom_app_Q

Proof. Machine-checked in Lean as D5/S3/HomologicalAlgebra/Solid/ExactDerivedHomologyNatural.exactDerivedHomologyNatIso_hom_app_Q (✓ 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.

Truth anchor: D5/S3/HomologicalAlgebra/Solid/ExactDerivedHomologyNatural.exactDerivedHomologyNatIso_hom_app_Q