mul_left

Mathlib.GroupTheory.SemidirectProduct

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

English

The multiplication in the semidirect product is given by (a,b) • (a’,b’) maps to (a φ(b) a’, b b’).

Русский

Умножение в полупрямом произведении задаётся формулой: (a,b)·(a',b') = (a φ(b)(a'), b b').

LaTeX

$$mul_def (a b) := ⟨a.1 * φ a.2 b.1, a.2 * b.2⟩$$

Lean4

@[simp]
theorem mul_left (a b : N ⋊[φ] G) : (a * b).left = a.left * φ a.right b.left :=
  rfl

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

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

Разделы

Аффилиация

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