English
If a scalar is central, then its right action is continuous when its left action is.
Русский
Если скаляр центральный, то правая деяние непрерывна, когда левая — непрерывна.
LaTeX
$$$\text{op}[SMul M^\mathrm{op} \alpha]\; \text{IsCentralScalar } M \alpha \Rightarrow \text{ContinuousConstSMul } M^\mathrm{op} \alpha$$$
Lean4
/-- If a scalar is central, then its right action is continuous when its left action is. -/
@[to_additive /-- If an additive action is central, then its right action is continuous when its
left action is. -/
]
instance op [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] : ContinuousConstSMul Mᵐᵒᵖ α :=
⟨MulOpposite.rec' fun c => by simpa only [op_smul_eq_smul] using continuous_const_smul c⟩
