one_right

Mathlib.GroupTheory.SemidirectProduct

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

English

In the semidirect product, the right projection of the unit is the identity in G: right(1) = 1.

Русский

В полупрямом произведении правый проекционный компонент единицы равен единице в G: right(1) = 1.

LaTeX

$$$\\pi_G(1_{N \\rtimes_{\\phi} G}) = 1_G$$$

Lean4

@[simp]
theorem one_right : (1 : N ⋊[φ] G).right = 1 :=
  rfl

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

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

Разделы

Аффилиация

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