Theorems · Theorem · group theory

Representation.linearize_single

∀ {k : Type u} {G : Type v} [inst : Monoid G] [inst_1 : Semiring k] {X : Action (Type w) G} (g : G) (x : X.V),
  ((Representation.linearize k G X) g) (MonoidAlgebra.single x 1) =
    MonoidAlgebra.single ((CategoryTheory.ConcreteCategory.hom (X.ρ g)) x) 1

Defined in

Mathlib.RepresentationTheory.Action

Cited by

1 results in Mathlib

Foundations

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

Assumes

MonoidSemiring