Theorems · Inductive type · group theory

Subrepresentation

{A : Type u_1} →
  {G : Type u_2} →
    {W : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : Monoid G] → [inst_2 : AddCommMonoid W] → [inst_3 : Module A W] → Representation A G W → Type u_3

A subrepresentation of G of the A-module W is a submodule of W which is stable under the G-action.

Defined in

Mathlib.RepresentationTheory.Subrepresentation

Cited by

23 results in Mathlib

Foundations

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

Assumes

SemiringMonoidAddCommMonoidModule