Theorems · Theorem · Lie groups

TopRep.hom_sub

∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G] (A B : TopRep k G)
  (f g : A ⟶ B), TopRep.Hom.hom (f - g) = TopRep.Hom.hom f - TopRep.Hom.hom g

Defined in

Mathlib.RepresentationTheory.Continuous.TopRep

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceRingMonoid