Theorems · Theorem · group theory

Rep.unit_iso_comm

∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] (V : Rep.{w, u, v} k G) (g : G) (x : ↑V),
  Rep.unitIsoAddEquiv ((V.ρ g).toFun x) =
    ((Rep.ofModuleMonoidAlgebra.obj (Rep.toModuleMonoidAlgebra.obj V)).ρ g).toFun (Rep.unitIsoAddEquiv x)

Defined in

Mathlib.RepresentationTheory.Rep.Iso

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingMonoid