ComplexShape

📁 Source: Mathlib/Algebra/Homology/SpectralSequence/ComplexShape.lean

Statistics

Metric	Count
Definitions ComplexShape, spectralSequenceFin, spectralSequenceNat	3
Theorems spectralSequenceFin_rel_iff, spectralSequenceNat_rel_iff	2
Total	5

ComplexShape

Definitions

Name	Category	Theorems
spectralSequenceFin 📖	CompOp	7 math math: CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin_deg, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin_i₃, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin_i₀, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin_i₂, spectralSequenceFin_rel_iff, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin_i₁, CategoryTheory.Abelian.SpectralObject.instHasSpectralSequenceFinHAddNatOfNatProdIntCoreE₂CohomologicalFin
spectralSequenceNat 📖	CompOp	13 math math: CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_deg, spectralSequenceNat_rel_iff, CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₂, CategoryTheory.Abelian.SpectralObject.instHasSpectralSequenceEIntProdNatCoreE₂HomologicalNat, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₂, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_deg, CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₀, CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₁, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₁, CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₃, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₀, CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₃, CategoryTheory.Abelian.SpectralObject.instHasSpectralSequenceEIntProdNatCoreE₂CohomologicalNat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
spectralSequenceFin_rel_iff 📖	mathematical	—	Rel spectralSequenceFin	—	—
spectralSequenceNat_rel_iff 📖	mathematical	—	Rel spectralSequenceNat	—	—

(root)

Definitions

Name	Category	Theorems
ComplexShape 📖	CompData	1 math math: ComplexShape.symm_bijective

---

← Back to Index