inv_left

Mathlib.GroupTheory.SemidirectProduct

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

English

For a ∈ N ⋊φ G, the left component of a^{-1} equals φ(a.right^{-1})(a.left^{-1}).

Русский

Для a = (n,g) из N ⋊φ G левая компонента a^{-1} равна φ(g^{-1})(n^{-1}).

LaTeX

$$$ a^{-1}.left = \\varphi(a.right^{-1})\\bigl(a.left^{-1}\\bigr) $$$

Lean4

@[simp]
theorem inv_left (a : N ⋊[φ] G) : a⁻¹.left = φ a.right⁻¹ a.left⁻¹ :=
  rfl

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

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

Разделы

Аффилиация

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