English
If there is a scalar action of R on A with IsScalarTower R A A, and A has a topology with continuous multiplication, then the constant-scalar action is continuous: ContinuousConstSMul R A.
Русский
Если существует скалярное действие R на A с условием IsScalarTower R A A и A имеет топологию с непрерывным умножением, тогда постоянное скалярное умножение непрерывно: ContinuousConstSMul R A.
LaTeX
$$$\\text{ContinuousConstSMul } R A$$$
Lean4
/-- If `R` acts on `A` via `A`, then continuous multiplication implies continuous scalar
multiplication by constants.
Notably, this instances applies when `R = A`, or when `[Algebra R A]` is available. -/
@[to_additive /-- If `R` acts on `A` via `A`, then continuous addition implies
continuous affine addition by constants. -/
]
instance (priority := 100) continuousConstSMul {R A : Type*} [Monoid A] [SMul R A] [IsScalarTower R A A]
[TopologicalSpace A] [ContinuousMul A] : ContinuousConstSMul R A where
continuous_const_smul
q := by
simp +singlePass only [← smul_one_mul q (_ : A)]
exact continuous_const.mul continuous_id
