instOne

Mathlib.GroupTheory.SemidirectProduct

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

English

Let N, G be groups and φ: G →* MulAut N. The semidirect product N ⋊φ G is a group with identity element (1_N, 1_G).

Русский

Пусть N, G — группы и φ: G →* MulAut N. Полупрямое произведение N ⋊φ G является группой, его единичный элемент равен (1_N, 1_G).

LaTeX

$$$1_{N \\rtimes_{\\phi} G} = (1_N,\\;1_G)$$$

Lean4

instance : One (SemidirectProduct N G φ) where one := ⟨1, 1⟩

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

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

Разделы

Аффилиация

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