Theorems · Definition · group theory

Rep.trivial

(k : Type u) →
  (G : Type v) →
    [inst : Semiring k] →
      [inst_1 : Monoid G] → (V : Type w) → [inst_2 : AddCommGroup V] → [Module k V] → Rep.{w, u, v} k G

The trivial k-linear G-representation on a k-module V.

Defined in

Mathlib.RepresentationTheory.Rep.Basic

Cited by

20 results in Mathlib

Foundations

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

Assumes

SemiringMonoidAddCommGroupModule