incl_range

Mathlib.Algebra.Lie.Subalgebra

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

English

The range of the inclusion map incl' of a Lie subalgebra K into L equals K.

Русский

Область значений включения incl' подалгебры K в L равна самой K.

LaTeX

$$$$\text{incl}.\text{range} = K.$$$$

Lean4

@[simp]
theorem incl_range : K.incl.range = K := by
  rw [← toSubmodule_inj]
  exact (K : Submodule R L).range_subtype

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

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

Разделы

Аффилиация

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