Theorems · Theorem · category theory

CategoryTheory.SpectralSequence.pageFunctor.congr_simp

∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C] {κ : Type u_2}
  (c : ℤ → ComplexShape κ) (r₀ r : ℤ) (hr : r₀ ≤ r),
  CategoryTheory.SpectralSequence.pageFunctor C c r₀ r hr = CategoryTheory.SpectralSequence.pageFunctor C c r₀ r hr

Defined in

Mathlib.Algebra.Homology.SpectralSequence.Basic

Cited by

0 results in Mathlib

Foundations

Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian