left_inl

Mathlib.GroupTheory.SemidirectProduct

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

English

For all n, left(inl(n)) = n.

Русский

Для любого n: левый компонент inl(n) равен n.

LaTeX

$$$\\text{left}(\\text{inl}(n)) = n$$$

Lean4

@[simp]
theorem left_inl (n : N) : (inl n : N ⋊[φ] G).left = n :=
  rfl

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

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

Разделы

Аффилиация

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