Theorems · Theorem · group theory

Rep.desc.congr_simp

∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G} [inst_2 : B.ρ.IsTrivial]
  (f f_1 : A ⟶ B), f = f_1 → Rep.desc f = Rep.desc f_1

Defined in

Mathlib.RepresentationTheory.Coinvariants

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingMonoidRepresentation.IsTrivial