coe_ofLe

Mathlib.Algebra.Lie.Subalgebra

URI: https://scilib.ai/kg/mathlib#LieSubalgebra.coe_ofLe

English

The underlying submodule of the constructed subalgebra of Le coincides with the range of the inclusion map.

Русский

Подмодуля основания подалгебры OfLe совпадает с образом включения.

LaTeX

$$$ (ofLe h).toSubmodule = LinearMap.range (Submodule.inclusion h) $$$

Lean4

@[simp]
theorem coe_ofLe : (ofLe h : Submodule R K') = LinearMap.range (Submodule.inclusion h) :=
  rfl

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

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

Разделы

Аффилиация

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