Main results 201 to 218

Declaration	Kind	Where	Note
CategoryTheory.QuadrantProductTotal.primitive_apply_early	theorem	HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 665
CategoryTheory.QuadrantProductTotal.nextHorizontalIndex_diag	theorem	HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 672
CategoryTheory.QuadrantProductTotal.nextVerticalIndex_diag_succ	theorem	HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 676
CategoryTheory.QuadrantProductTotal.nextVerticalIndex_diag_first_early	theorem	HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 682
CategoryTheory.QuadrantProductTotal.primitive_boundary_index	theorem	HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 690
CategoryTheory.QuadrantProductTotal.acyclic_productTotal	theorem	HomologicalAlgebra/Homology/ProductTotalAcyclicity.lean, line 756
CategoryTheory.AdmissibleLayer	structure	HomologicalAlgebra/Abelian/AdmissibleLayers.lean, line 40
CategoryTheory.AdmissibleLayer.LowerBounded	abbrev	HomologicalAlgebra/Abelian/AdmissibleLayers.lean, line 71
CategoryTheory.AdmissibleLayer.lowerInclusion	def	HomologicalAlgebra/Abelian/AdmissibleLayers.lean, line 75
CategoryTheory.AdmissibleLayer.lowerInclusion_monotone	theorem	HomologicalAlgebra/Abelian/AdmissibleLayers.lean, line 80
CategoryTheory.AdmissibleLayer.lowerCut	def	HomologicalAlgebra/Abelian/AdmissibleLayers.lean, line 88
CategoryTheory.AdmissibleLayer.lowerCut_lower	theorem	HomologicalAlgebra/Abelian/AdmissibleLayers.lean, line 100
CategoryTheory.AdmissibleLayer.lowerCut_upper	theorem	HomologicalAlgebra/Abelian/AdmissibleLayers.lean, line 104
CategoryTheory.AdmissibleLayer.lowerCut_galoisConnection	theorem	HomologicalAlgebra/Abelian/AdmissibleLayers.lean, line 109
CategoryTheory.AdmissibleLayer.lowerCut_monotone	theorem	HomologicalAlgebra/Abelian/AdmissibleLayers.lean, line 121
CategoryTheory.AdmissibleLayer.le_lowerInclusion_lowerCut	theorem	HomologicalAlgebra/Abelian/AdmissibleLayers.lean, line 126
CategoryTheory.AdmissibleLayer.lowerCut_lowerInclusion	theorem	HomologicalAlgebra/Abelian/AdmissibleLayers.lean, line 133
CategoryTheory.AdmissibleLayer.lowerCutAdjunction	def	HomologicalAlgebra/Abelian/AdmissibleLayers.lean, line 142

Quoted from the main results in formalization.yaml of FormalFrontier/homological-algebra at commit 8bcaebe9, Apache-2.0.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.