Theorems · Theorem · group theory

Representation.linearize_apply

∀ (k : Type u) (G : Type v) [inst : Monoid G] [inst_1 : Semiring k] (X : Action (Type w) G) (g : G),
  (Representation.linearize k G X) g =
    MonoidAlgebra.mapDomainLinearMap k k ⇑(CategoryTheory.ConcreteCategory.hom (X.ρ g))

Defined in

Mathlib.RepresentationTheory.Action

Cited by

1 results in Mathlib

Foundations

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

Assumes

MonoidSemiring