lieSpan_eq

Mathlib.Algebra.Lie.Submodule

URI: https://scilib.ai/kg/mathlib#LieSubmodule.lieSpan_eq

English

For any LieSubmodule N, lieSpan R L (N as a Set M) equals N.

Русский

Для любого Lie-подмодуля N, lieSpan(R,L,(N : Set M)) = N.

LaTeX

$$lieSpan_{R,L}(N:\\Set M) = N$$

Lean4

theorem lieSpan_eq (N : LieSubmodule R L M) : lieSpan R L (N : Set M) = N :=
  le_antisymm (lieSpan_le.mpr rfl.subset) subset_lieSpan

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

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

Разделы

Аффилиация

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