leibniz

Mathlib.RingTheory.Derivation.Basic

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

English

Generalization of smul-compatibility when fields/structures are layered: D(r·a) = r·D(a) for suitable scalar r from S.

Русский

Обобщение совместимости умножения на скаляр в многоуровневых структурах: D(r·a) = r·D(a) для подходящих скаляров r из S.

LaTeX

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

Lean4

@[simp]
theorem leibniz : D (a * b) = a • D b + b • D a :=
  D.leibniz' _ _

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

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

Разделы

Аффилиация

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