apply

Mathlib.Algebra.Lie.Derivation.Basic

URI: https://scilib.ai/kg/mathlib#LieDerivation.Simps.apply

English

There is a linear-map structure for LieDerivation, respecting addition and scalar multiplication.

Русский

Существует линейно-отображающее ядро для LieDerivation, сохраняющее сложение и умножение на скаляр.

LaTeX

$$instance: LinearMapClass (LieDerivation R L M) R L M$$

Lean4

/-- See Note [custom simps projection] -/
def apply (D : LieDerivation R L M) : L → M :=
  D

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

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

Разделы

Аффилиация

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