map_inr

Mathlib.GroupTheory.SemidirectProduct

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

English

Define a semidirect product congruence without specifying φ₂.

Русский

Определить конгруэнцию полупрямого произведения без задания φ₂.

LaTeX

$$$ congr' : N_1 ⋊[φ_1] G_1 \to N_2 ⋊[φ_2] G_2 $ with φ₂ given by conjugation$$

Lean4

@[simp]
theorem map_inr (g : G₁) : map fn fg h (inr g) = inr (fg g) := by simp [map]

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

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

Разделы

Аффилиация

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