Theorems · Theorem · Lie groups

TopRep.ofHom_add

∀ {k : Type u} {G : Type v} {X Y : Type w} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G]
  [inst_3 : AddCommGroup X] [inst_4 : Module k X] [inst_5 : TopologicalSpace X] [inst_6 : IsTopologicalAddGroup X]
  [inst_7 : ContinuousSMul k X] [inst_8 : AddCommGroup Y] [inst_9 : Module k Y] [inst_10 : TopologicalSpace Y]
  [inst_11 : IsTopologicalAddGroup Y] [inst_12 : ContinuousSMul k Y] {ρ : ContRepresentation k G X}
  {σ : ContRepresentation k G Y} (f g : ContIntertwiningMap ρ σ), TopRep.ofHom (f + g) = TopRep.ofHom f + TopRep.ofHom g

Defined in

Mathlib.RepresentationTheory.Continuous.TopRep

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceRingMonoidAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMulAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMul