one_left

Mathlib.GroupTheory.SemidirectProduct

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

English

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

Русский

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

LaTeX

$$$\\pi_N(1_{N \\rtimes_{\\phi} G}) = 1_N$$$

Lean4

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

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

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

Разделы

Аффилиация

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