inr

Mathlib.GroupTheory.SemidirectProduct

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

← MathLib Explorer

English

The map inr: G → N ⋊φ G sends g to (1,g) and is a MonoidHom.

Русский

Отображение inr: G → N ⋊φ G отправляет g в (1,g) и является моноидом-гомоморфизмом.

LaTeX

$$$\\text{inr}(g) = (1,g)$$$

Lean4

/-- The canonical map `G →* N ⋊[φ] G` sending `g` to `⟨1, g⟩` -/
def inr : G →* N ⋊[φ] G where
  toFun g := ⟨1, g⟩
  map_one' := rfl
  map_mul' := by intros; ext <;> simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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