continuousConstSMul — Mathlib

English

If M acts on α with continuous constant smul, then the same holds for the group of units Mˣ acting on α.

Русский

Если моноид M действует на α с непрерывным константным умножением, то та же самая структура существует и для группы единиц Mˣ, действующей на α.

LaTeX

$$$ \\mathrm{ContinuousConstSMul}(M, \\alpha) \\Rightarrow \\mathrm{ContinuousConstSMul}(M^{\\times}, \\alpha) $$$

Lean4

@[to_additive]
instance continuousConstSMul : ContinuousConstSMul Mˣ α where continuous_const_smul m := continuous_const_smul (m : M)

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