Theorems · Definition · group theory

Representation.ofMulActionSubsingletonEquivTrivial

(k : Type u) →
  [inst : Semiring k] →
    (G : Type v) →
      [inst_1 : Monoid G] →
        (H : Type w) →
          [Subsingleton H] →
            [MulOneClass H] →
              [inst_4 : MulAction G H] → (Representation.ofMulAction k G H).Equiv (Representation.trivial k G k)

If there exists G-action on a trivial monoid H then the induced representation on k[H] is equivalent to the trivial representation.

Defined in

Mathlib.RepresentationTheory.Equiv

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringMonoidSubsingletonMulOneClassMulAction