mul_right

Mathlib.GroupTheory.SemidirectProduct

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

English

Right component of the product in a semidirect product is just the product of the right components.

Русский

Правая часть произведения в полупрямом произведении равна произведению правых компонент.

LaTeX

$$mul_right (a b) : (a*b).right = a.right * b.right$$

Lean4

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

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

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

Разделы

Аффилиация

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