Theorems · Theorem · category theory

CategoryTheory.ComposableArrows.sc.congr_simp

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} (S S_1 : CategoryTheory.ComposableArrows C n) (e_S : S = S_1) (hS : S.IsComplex) (i i_1 : ℕ) (e_i : i = i_1)
  (hi : i + 2 ≤ n), S.sc hS i hi = S_1.sc ⋯ i_1 ⋯

Defined in: Mathlib.Algebra.Homology.SpectralObject.Homology
Cited by: 0 results in Mathlib
Foundations: Depth 58 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.Category CategoryTheory.Limits.HasZeroMorphisms

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.Limits.HasZeroMorphismsstatement and proof · cited by 3,275
CategoryTheory.ShortComplexstatement · cited by 1,850
CategoryTheory.ComposableArrowsstatement and proof · cited by 627
CategoryTheory.ComposableArrows.IsComplexstatement and proof · cited by 37
CategoryTheory.ComposableArrows.scstatement and proof · cited by 16

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.