Theorems · Theorem · group theory

Rep.indCoindIso_inv_hom_toLinearMap

∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] [inst_3 : S.FiniteIndex] (A : Rep.{max w u, u, v} k ↥S),
  (Rep.Hom.hom A.indCoindIso.inv).toLinearMap =
    { toFun := (Representation.Equiv.mk (LinearEquiv.ofLinearMap A.indToCoind A.coindToInd ⋯ ⋯) ⋯).invFun,
      map_add' := ⋯, map_smul' := ⋯ }

Defined in

Mathlib.RepresentationTheory.FiniteIndex

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingGroupDecidableRelSubgroup.FiniteIndex