liftAux_map_add

Mathlib.Algebra.Lie.Free

URI: https://scilib.ai/kg/mathlib#FreeLieAlgebra.liftAux_map_add

English

The liftAux map respects scalar multiplication: liftAux(R,f)(t • a) = t • liftAux(R,f)(a).

Русский

Функция liftAux сохраняет умножение на скаляры: liftAux(R,f)(t • a) = t • liftAux(R,f)(a).

LaTeX

$$$\mathrm{liftAux}(R,f)(t \cdot a) = t \cdot \mathrm{liftAux}(R,f)(a).$$$

Lean4

theorem liftAux_map_add (f : X → L) (a b : lib R X) : liftAux R f (a + b) = liftAux R f a + liftAux R f b :=
  NonUnitalAlgHom.map_add _ a b

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

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

Разделы

Аффилиация

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