smul_opposite_mul

Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

URI: https://scilib.ai/kg/mathlib#Subgroup.smul_opposite_mul

English

For any H ≤ G and x,g ∈ G, and h ∈ H.op, the action satisfies h • (g x) = g • (h • x).

Русский

Для любого H ≤ G, x,g ∈ G и h ∈ H^{op} выполнено: h • (g x) = g • (h • x).

LaTeX

$$$h \cdot (g x) = g \cdot (h \cdot x)$$$

Lean4

@[to_additive]
theorem smul_opposite_mul {H : Subgroup G} (x g : G) (h : H.op) : h • (g * x) = g * h • x :=
  mul_assoc _ _ _

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

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

Разделы

Аффилиация

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