English
If the SMul action commutes with left multiplication (SMulCommClass), then continuous multiplication implies continuous scalar multiplication by constants.
Русский
Если действие умножения согласуется с левой умножением (SMulCommClass), то непрерывность умножения и константного скаляра подразумевает непрерывность скалярного умножения.
LaTeX
$$$\\text{ContinuousConstSMul } R A$$$
Lean4
/-- If the action of `R` on `A` commutes with left-multiplication, then continuous multiplication
implies continuous scalar multiplication by constants.
Notably, this instances applies when `R = Aᵐᵒᵖ`. -/
@[to_additive /-- If the action of `R` on `A` commutes with left-addition, then
continuous addition implies continuous affine addition by constants.
Notably, this instances applies when `R = Aᵃᵒᵖ`. -/
]
instance (priority := 100) continuousConstSMul {R A : Type*} [Monoid A] [SMul R A] [SMulCommClass R A A]
[TopologicalSpace A] [ContinuousMul A] : ContinuousConstSMul R A where
continuous_const_smul
q := by
simp +singlePass only [← mul_smul_one q (_ : A)]
exact continuous_id.mul continuous_const
