Theorems · Definition · group theory

Representation.linearizeOfMulActionIso

(k : Type u) →
  (G : Type v) →
    [inst : Monoid G] →
      [inst_1 : Semiring k] →
        (H : Type w) →
          [inst_2 : MulAction G H] →
            (Representation.linearize k G (Action.ofMulAction G H)).Equiv (Representation.ofMulAction k G H)

This a type-changing equivalence to avoid abusing defeq.

Defined in

Mathlib.RepresentationTheory.Action

Cited by

0 results in Mathlib

Foundations

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

Assumes

MonoidSemiringMulAction