map_comp_inr

Mathlib.GroupTheory.SemidirectProduct

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

English

Define a semidirect product congruence from fn, fg and h.

Русский

Определить конгруэнцию полупрямого произведения из fn, fg и h.

LaTeX

$$$ congr : N_1 ⋊[φ_1] G_1 ≃* N_2 ⋊[φ_2] G_2 $ under h$$

Lean4

@[simp]
theorem map_comp_inr : (map fn fg h).comp inr = inr.comp fg := by ext <;> simp [map]

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

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

Разделы

Аффилиация

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