instSMul — Mathlib

English

If M acts on G via a SMul action, then Germ_l G carries an SMul action of M, defined by applying the action pointwise through representatives.

Русский

Если M действует на G через действие SMul, то Germ_l G наследует действие SMul от M, задаваемое через применение действия по позиции представителя.

LaTeX

$$$[SMul\\ M\\ G] \\Rightarrow SMul\\ M\\ (\\mathrm{Germ}_l G).$$$

Lean4

@[to_additive]
instance instSMul [SMul M G] : SMul M (Germ l G) where smul n := map (n • ·)

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