coe_smul — Mathlib

English

The underlying function of the scaled derivation r • D is the scalar multiple of the original function: ↑(r • D) = r • ↑D.

Русский

Пусть D — деривация, а скаляр r из S. Тогда соответствующая ей функция удовлетворяет: ↑(r • D) = r • ↑D.

LaTeX

$$$\uparrow\bigl(r \cdot D\bigr) = r \cdot \uparrow D,$$$

Lean4

@[simp]
theorem coe_smul (r : S) (D : Derivation R A M) : ⇑(r • D) = r • ⇑D :=
  rfl

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