instAdd

Mathlib.Algebra.Lie.Basic

URI: https://scilib.ai/kg/mathlib#LieModuleHom.instAdd

English

The inverse map defined as above preserves the Lie bracket action: g⁅x,n⁆ = ⁅x,g n⁆.

Русский

Обратная карта сохраняет скобочную операцию Ли: g⁅x,n⁆ = ⁅x, g n⁆.

LaTeX

$$∀ x ∈ L, n ∈ N, g⁅x,n⁆ = ⁅x, g n⁆$$

Lean4

instance : Add (M →ₗ⁅R,L⁆ N) where add f g := { (f : M →ₗ[R] N) + (g : M →ₗ[R] N) with map_lie' := by simp }

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

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

Разделы

Аффилиация

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