Theorems · Theorem · group theory

Representation.IntertwiningMap.mk.injEq

∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (toLinearMap : V →ₗ[A] W)
  (isIntertwining' : ∀ (g : G), toLinearMap ∘ₗ ρ g = σ g ∘ₗ toLinearMap) (toLinearMap_1 : V →ₗ[A] W)
  (isIntertwining'_1 : ∀ (g : G), toLinearMap_1 ∘ₗ ρ g = σ g ∘ₗ toLinearMap_1),
  ({ toLinearMap := toLinearMap, isIntertwining' := isIntertwining' } =
      { toLinearMap := toLinearMap_1, isIntertwining' := isIntertwining'_1 }) =
    (toLinearMap = toLinearMap_1)

Defined in

Mathlib.RepresentationTheory.Intertwining

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringMonoidAddCommMonoidAddCommMonoidModuleModule