Theorems · Theorem · group theory

Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eq

∀ (k G : Type u) [inst : CommRing k] (n : ℕ) [inst_1 : Group G],
  CategoryTheory.CategoryStruct.comp (Rep.barComplex.d k G n) (Rep.diagonalSuccIsoFree k G n).inv =
    CategoryTheory.CategoryStruct.comp (Rep.diagonalSuccIsoFree k G (n + 1)).inv ((Rep.standardComplex k G).d (n + 1) n)

Defined in: Mathlib.RepresentationTheory.Homological.Resolution
Cited by: 0 results in Mathlib
Foundations: Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing Group

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites74

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

DFunLike.coeproof · cited by 62,936
Quiver.Homstatement · cited by 32,603
CategoryTheory.CategoryStruct.compstatement and proof · cited by 17,999
CommRingstatement and proof · cited by 17,173
Semiringproof · cited by 13,802
CategoryTheory.Iso.invstatement and proof · cited by 6,514
Groupstatement and proof · cited by 6,238
Finset.sumproof · cited by 5,195
CategoryTheory.ConcreteCategory.homproof · cited by 4,022
Monoidproof · cited by 3,887
Finset.univproof · cited by 3,473
CategoryTheory.MonoidalCategoryStruct.tensorObjproof · cited by 3,106

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.