Theorems · Theorem · group theory

Representation.ofMulActionSelfAsModuleEquiv_apply

∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Group G]
  (a : (Representation.ofMulAction k G G).asModule),
  Representation.ofMulActionSelfAsModuleEquiv a = (Representation.ofMulAction k G G).asModuleEquiv.toAddEquiv.toFun a

Defined in

Mathlib.RepresentationTheory.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringGroup