instContinuousSMul — Mathlib

English

Scalar multiplication on MvPowerSeries is continuous in the given topology.

Русский

Умножение на скаляры на MvPowerSeries непрерывно в данной топологии.

LaTeX

$$ContinuousSMul R (MvPowerSeries σ S)$$

Lean4

/-- Scalar multiplication on `MvPowerSeries` is continuous. -/
instance {S : Type*} [Semiring S] [TopologicalSpace S] [CommSemiring R] [Algebra R S] [ContinuousSMul R S] :
    ContinuousSMul R (MvPowerSeries σ S) :=
  instContinuousSMulForall

Похожие утверждения