smul_lie

Mathlib.Algebra.Lie.Basic

URI: https://scilib.ai/kg/mathlib#smul_lie

English

There is a Lie tower structure on L acting on M, i.e., the Leibniz identity holds for the pair (L,M).

Русский

Для пары Ли-модуля L, M существует структура IsLieTower, удовлетворяющая законам Ли-структуры.

LaTeX

$$$\\text{IsLieTower } L\\; L\\; M$ with Leibniz_lie$$

Lean4

@[simp]
theorem smul_lie : ⁅t • x, m⁆ = t • ⁅x, m⁆ :=
  LieModule.smul_lie t x m

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

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

Разделы

Аффилиация

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