instContinuousMulMultiplicativeOfContinuousAdd

English

If M has an additive structure with continuous addition, then the multiplicative structure on Multiplicative M has continuous multiplication.

Русский

Если в M есть аддитивная структура с непрерывным сложением, то умножение в Multiplicative M непрерывно.

LaTeX

$$$\\text{ContinuousMul}(\\text{Multiplicative } M)$, когда $M$ имеет непрерывное сложение$$

Lean4

instance [TopologicalSpace M] [Add M] [ContinuousAdd M] : ContinuousMul (Multiplicative M) where
  continuous_mul := @continuous_add M _ _ _

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