Theorems · Theorem · group theory

Rep.indToCoindAux_comm

∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] {A B : Rep.{u_1, u, v} k ↥S} (f : A ⟶ B) (g₁ g₂ : G) (a : ↑A),
  (B.indToCoindAux g₁) ((Rep.Hom.hom f) a) g₂ = (Rep.Hom.hom f) ((A.indToCoindAux g₁) a g₂)

Defined in

Mathlib.RepresentationTheory.FiniteIndex

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingGroupDecidableRel