map_smul

Mathlib.RingTheory.Derivation.Basic

URI: https://scilib.ai/kg/mathlib#Derivation.map_smul

English

D(r · a) = r · D(a) for all r in R, a in A.

Русский

Производная respects scalar multiplication: D(r·a) = r·D(a).

LaTeX

$$$D(r \cdot a) = r \cdot D(a).$$$

Lean4

@[simp]
theorem map_smul : D (r • a) = r • D a :=
  D.toLinearMap.map_smul r a

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru