range_subset_idealRange

Mathlib.Algebra.Lie.Ideal

URI: https://scilib.ai/kg/mathlib#LieHom.range_subset_idealRange

English

For a LieHom f, every element of the range lies in the idealRange of f.

Русский

Для гомоморфизма Ли f каждый элемент образа принадлежит idealRange(f).

LaTeX

$$$\\text{range}(f) \\subseteq \\text{idealRange}(f)$$$

Lean4

theorem range_subset_idealRange : (f.range : Set L') ⊆ f.idealRange :=
  LieSubmodule.subset_lieSpan

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

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

Разделы

Аффилиация

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