toGroupExtension_inl

Mathlib.GroupTheory.GroupExtension.Defs

URI: https://scilib.ai/kg/mathlib#SemidirectProduct.toGroupExtension_inl

English

The inl component of the semidirect-induced group extension equals the standard inl map.

Русский

Компонента inl у группы-расширения, полученной из полупростого произведения, совпадает с обычной функцией inl.

LaTeX

$$$ (toGroupExtension\\; \\varphi).inl = Inl $$$

Lean4

theorem toGroupExtension_inl : (toGroupExtension φ).inl = SemidirectProduct.inl :=
  rfl

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

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

Разделы

Аффилиация

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