Theorems · Theorem · Lie groups

TopRep.of_V

∀ {k : Type u} {G : Type v} (X : 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] (ρ : ContRepresentation k G X), ↑(TopRep.of ρ) = X

Defined in

Mathlib.RepresentationTheory.Continuous.TopRep

Cited by

0 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

TopologicalSpaceRingMonoidAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMul