inl_aut

Mathlib.GroupTheory.SemidirectProduct

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

English

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

Русский

Согласование: inl(φ(g)(n)) = inr(g) · inl(n) · inr(g)^{-1}.

LaTeX

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

Lean4

theorem inl_aut (g : G) (n : N) : (inl (φ g n) : N ⋊[φ] G) = inr g * inl n * inr g⁻¹ := by ext <;> simp

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

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

Разделы

Аффилиация

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