coe_smul — Mathlib

English

For any SMul action of M on G, the coercion map commutes with the SMul action, i.e., the germ of n • f equals n • (the germ of f).

Русский

Для любого действия M на G через SMul отображение сопряжения сохраняет действие: жермa n • f равна жерме (n • f).

LaTeX

$$$[SMul\\ M\\ G] \\Rightarrow \\uparrow(n \\cdot f) = n \\cdot (f^{\\uparrow}).$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_smul [SMul M G] (n : M) (f : α → G) : ↑(n • f) = n • (f : Germ l G) :=
  rfl

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