Theorems · Theorem · group theory

Rep.mkIso_hom_hom_apply

∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {X Y : Type w} [inst_2 : AddCommGroup X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module k X] [inst_5 : Module k Y] {ρ : Representation k G X}
  {σ : Representation k G Y} (e : ρ.Equiv σ) (x : X), (Rep.Hom.hom (Rep.mkIso e).hom) x = (↑e).toLinearMap x

Defined in

Mathlib.RepresentationTheory.Rep.Basic

Cited by

0 results in Mathlib

Foundations

Depth 51 from the axioms · uses propext, Quot.sound

Assumes

SemiringMonoidAddCommGroupAddCommGroupModuleModule