Theorems · Definition · group theory

Rep.ofMulActionSubsingletonIsoTrivial

(k : Type u) →
  (G : Type v) →
    [inst : Ring k] →
      [inst_1 : Monoid G] →
        (H : Type u) →
          [Subsingleton H] → [MulOneClass H] → [inst_4 : MulAction G H] → Rep.ofMulAction k G H ≅ Rep.trivial k G k

When H = {1}, the G-representation on k[H] induced by an action of G on H is isomorphic to the trivial representation on k.

Defined in

Mathlib.RepresentationTheory.Rep.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

RingMonoidSubsingletonMulOneClassMulAction