Theorems · Theorem · group theory

Rep.invariantsAdjunction_counit_app

∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Group G] (X : Rep.{u_1, u, v} k G),
  (Rep.invariantsAdjunction k G).counit.app X =
    Rep.ofHom { toLinearMap := X.ρ.invariants.subtype, isIntertwining' := ⋯ }

Defined in

Mathlib.RepresentationTheory.Invariants

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingGroup