rightHom_comp_inl

Mathlib.GroupTheory.SemidirectProduct

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

English

Underlying function of rightHom is the right projection. (2)

Русский

Функция, лежащая в основании rightHom, — правая проекция. (2)

LaTeX

$$$ rightHom = right $$$

Lean4

@[simp]
theorem rightHom_comp_inl : (rightHom : N ⋊[φ] G →* G).comp inl = 1 := by ext; simp [rightHom]

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

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

Разделы

Аффилиация

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