inl_aut_inv

Mathlib.GroupTheory.SemidirectProduct

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

English

A related inverse relation holds with φ(g)^{-1}: inl(φ(g)^{-1}(n)) = inr(g)^{-1} · inl(n) · inr(g).

Русский

Соотношение обратного аналогично: inl(φ(g)^{-1}(n)) = inr(g)^{-1} · inl(n) · inr(g).

LaTeX

$$inl(φ(g)^{-1}(n)) = inr(g)^{-1} · inl(n) · inr(g)$$

Lean4

theorem inl_aut_inv (g : G) (n : N) : (inl ((φ g)⁻¹ n) : N ⋊[φ] G) = inr g⁻¹ * inl n * inr g := by
  rw [← MonoidHom.map_inv, inl_aut, inv_inv]

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

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

Разделы

Аффилиация

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