Theorems · Theorem · group theory

Rep.indToCoindAux_snd_mul_inv

∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Group G] {S : Subgroup G}
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] {A : Rep.{w, u, v} k ↥S} (g₁ g₂ g₃ : G) (a : ↑A),
  (A.indToCoindAux g₁) a (g₂ * g₃⁻¹) = (A.indToCoindAux (g₁ * g₃)) a g₂

Defined in

Mathlib.RepresentationTheory.FiniteIndex

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingGroupDecidableRel