Theorems · Theorem · group theory

groupHomology.inhomogeneousChains.d_comp_d

∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (n : ℕ),
  CategoryTheory.CategoryStruct.comp (groupHomology.inhomogeneousChains.d A (n + 1))
      (groupHomology.inhomogeneousChains.d A n) =
    0

Defined in: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 113 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.

Cites13

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

Quiver.Homstatement · cited by 32,603
CategoryTheory.CategoryStruct.compstatement and proof · cited by 17,999
CommRingstatement and proof · cited by 17,173
Groupstatement and proof · cited by 6,238
Finsuppstatement · cited by 5,255
CategoryTheory.Category.id_compproof · cited by 1,998
ModuleCatstatement · cited by 1,429
Repstatement and proof · cited by 843
Rep.Vstatement · cited by 695
ModuleCat.ofstatement · cited by 594
groupHomology.inhomogeneousChainsproof · cited by 90
HomologicalComplex.d_comp_dproof · cited by 36

Cited by1

Results whose statement or proof uses this declaration.

groupHomology.d₃₂_comp_d₂₁proof · cited by 4