Theorems · Theorem · group theory

Representation.freeLiftLEquiv_apply

∀ {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') (f : (Representation.free k G α).IntertwiningMap σ)
  (i : α), (σ.freeLiftLEquiv α) f i = f fun₀ | i => MonoidAlgebra.single 1 1

Defined in

Mathlib.RepresentationTheory.Equiv

Cited by

0 results in Mathlib

Foundations

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

Assumes

MonoidAddCommMonoidCommSemiringModule