op_smul_op_smul — Mathlib

English

Let β be a type with a right action of α; then b <• a1 <• a2 = b <• (a1 * a2). This expresses associativity of the right action.

Русский

Пусть β имеет правое действие α; тогда b <• a1 <• a2 = b <• (a1 a2). Это выражает ассоциативность правого действия.

LaTeX

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

Lean4

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

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