Theorems · Theorem · group theory

Representation.ofCoinvariantsTprodLeftRegular_mk_tmul_single

∀ {k : Type u_6} {G : Type u_7} {V : Type u_8} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (x : V) (g : G) (r : k),
  ρ.ofCoinvariantsTprodLeftRegular
      ((Representation.Coinvariants.mk (ρ.tprod (Representation.leftRegular k G))) (x ⊗ₜ[k] MonoidAlgebra.single g r)) =
    r • (ρ g⁻¹) x

Defined in

Mathlib.RepresentationTheory.Coinvariants

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingGroupAddCommGroupModule