Theorems · Theorem · group theory

Representation.Coinvariants.mk_tmul_inv

∀ {k : Type u_6} {G : Type u_7} {V : Type u_8} {W : Type u_9} [inst : CommRing k] [inst_1 : Group G]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  (ρ : Representation k G V) (τ : Representation k G W) (x : V) (y : W) (g : G),
  (Representation.Coinvariants.mk (ρ.tprod τ)) (x ⊗ₜ[k] (τ g⁻¹) y) =
    (Representation.Coinvariants.mk (ρ.tprod τ)) ((ρ g) x ⊗ₜ[k] y)

Defined in

Mathlib.RepresentationTheory.Coinvariants

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingGroupAddCommGroupModuleAddCommGroupModule