Theorems · Definition · group theory

Representation.asModule

{k : Type u_4} →
  {G : Type u_5} →
    {V : Type u_6} →
      [inst : Semiring k] →
        [inst_1 : Monoid G] → [inst_2 : AddCommMonoid V] → [inst_3 : Module k V] → Representation k G V → Type u_6

If ρ : Representation k G V, then ρ.asModule is a type synonym for V, which we equip with an instance Module k[G] ρ.asModule. You should use asModuleEquiv : ρ.asModule ≃+ V to translate terms.

Defined in

Mathlib.RepresentationTheory.Basic

Cited by

22 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext, Quot.sound

Assumes

SemiringMonoidAddCommMonoidModule