English
If a scalar action is central, then the right action is uniform continuous whenever the left action is. This transfers to uniform-continuous structures on opposite types as well.
Русский
Если действие скаляра центрально, то правое действие равномерно непрерывно, когда левое — так же. Это переносится на противоположные типы.
LaTeX
$$$\text{op}$-instance with IsCentralScalar$$$
Lean4
/-- If a scalar action is central, then its right action is uniform continuous when its left action
is. -/
@[to_additive /-- If an additive action is central, then its right action is uniform
continuous when its left action is. -/
]
instance (priority := 100) op [SMul Mᵐᵒᵖ X] [IsCentralScalar M X] [UniformContinuousConstSMul M X] :
UniformContinuousConstSMul Mᵐᵒᵖ X :=
⟨MulOpposite.rec' fun c ↦ by simpa only [op_smul_eq_smul] using uniformContinuous_const_smul c⟩
