Theorems · Theorem · group theory

Rep.FiniteCyclicGroup.resolution_complex

∀ (k : Type u) {G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (g : G)
  (hg : ∀ (x : G), x ∈ Subgroup.zpowers g),
  (Rep.FiniteCyclicGroup.resolution k g hg).complex =
    (Rep.FiniteCyclicGroup.chainComplexFunctor k g).obj (Rep.leftRegular k G)

Defined in: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Cited by: 0 results in Mathlib
Foundations: Depth 111 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing CommGroup Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites14

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

CategoryTheory.Functor.objstatement · cited by 19,642
CommRingstatement and proof · cited by 17,173
Fintypestatement and proof · cited by 7,736
Subgroupstatement · cited by 3,593
CommGroupstatement and proof · cited by 990
Repstatement · cited by 843
ComplexShape.downstatement · cited by 605
ChainComplexstatement · cited by 350
Subgroup.zpowersstatement and proof · cited by 204
CategoryTheory.ProjectiveResolution.complexstatement and proof · cited by 82
Rep.trivialstatement · cited by 20
Rep.leftRegularstatement · cited by 19

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.