Theorems · Definition · group theory

Representation

(k : Type u_1) →
  (G : Type u_2) →
    (V : Type u_3) → [inst : Semiring k] → [Monoid G] → [inst_2 : AddCommMonoid V] → [Module k V] → Type (max u_2 u_3)

A representation of G on the k-module V is a homomorphism G →* (V →ₗ[k] V).

Defined in

Mathlib.RepresentationTheory.Basic

Cited by

396 results in Mathlib

Foundations

Depth 32 from the axioms, rests on 357 definitions · uses propext, Quot.sound

Assumes

SemiringMonoidAddCommMonoidModule