Theorems · Theorem · group theory

Representation.freeLift_single_single

∀ {G : Type v} [inst : Monoid G] {V : Type v'} [inst_1 : AddCommMonoid V] {k : Type u} [inst_2 : CommSemiring k]
  [inst_3 : Module k V] (σ : Representation k G V) {α : Type w'} (i : α) (g : G) (r : k) (f : α → V),
  ((σ.freeLift f) fun₀ | i => MonoidAlgebra.single g r) = r • (σ g) (f i)

Defined in

Mathlib.RepresentationTheory.Equiv

Cited by

1 results in Mathlib

Foundations

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

Assumes

MonoidAddCommMonoidCommSemiringModule