op_smul_mul

Mathlib.Algebra.Group.Action.Opposite

URI: https://scilib.ai/kg/mathlib#op_smul_mul

English

For b ∈ β and a1,a2 ∈ α, the action satisfies b <• (a1 * a2) = (b <• a2) <• a1.

Русский

Для b ∈ β и a1,a2 ∈ α выполнено b <• (a1 * a2) = (b <• a2) <• a1.

LaTeX

$$$\forall b\in \beta, a_1,a_2\in \alpha:\; b <\cdot (a_1 a_2) = (b <\cdot a_2) <\cdot a_1$$$

Lean4

@[to_additive]
theorem op_smul_mul (b : β) (a₁ a₂ : α) : b <• (a₁ * a₂) = b <• a₁ <• a₂ :=
  mul_smul _ _ _

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

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

Разделы

Аффилиация

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