const_smul — Mathlib

English

The germ construction respects the SMul action on constants: for any n ∈ M and a ∈ G, the germ of n • a equals n • (germ of a).

Русский

Конструкция жермов сохраняет действие множителя на константах: для любого n ∈ M и a ∈ G, жермa (n • a) равна n • жерма a.

LaTeX

$$$[SMul\\ M\\ G] \\Rightarrow \\uparrow(n \\cdot a) = n \\cdot \\uparrow a.$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem const_smul [SMul M G] (n : M) (a : G) : (↑(n • a) : Germ l G) = n • (↑a : Germ l G) :=
  rfl

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