add_apply

Mathlib.Algebra.Lie.Derivation.Basic

URI: https://scilib.ai/kg/mathlib#LieDerivation.add_apply

English

The action of the sum of two derivations on an element is the sum of their actions: (D1 + D2) a = D1 a + D2 a.

Русский

Действие суммы двух дериваторов на элемент равно сумме их действий: (D1 + D2) a = D1 a + D2 a.

LaTeX

$$$\forall a, (D_1 + D_2)\ a = D_1\ a + D_2\ a$$$

Lean4

theorem add_apply : (D1 + D2) a = D1 a + D2 a :=
  rfl

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

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

Разделы

Аффилиация

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