Theorems · Definition · Lie groups

ContinuousMap.mulRight

{X : Type u_5} → [inst : TopologicalSpace X] → [inst_1 : Mul X] → [SeparatelyContinuousMul X] → X → C(X, X)

The continuous map fun y => y * x

Defined in

Mathlib.Topology.Algebra.Monoid

Cited by

4 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

TopologicalSpaceMulSeparatelyContinuousMul