smul_assoc — Mathlib

English

If M,N act on α with a tower IsScalarTower, then the associativity of the action holds: (x • y) • z = x • (y • z).

Русский

Если M,N действуют на α образуя башню IsScalarTower, то выполняется ассоциативность действия: (x • y) • z = x • (y • z).

LaTeX

$$$ (x \cdot y) \cdot z = x \cdot (y \cdot z). $$$

Lean4

@[to_additive (attr := simp)]
theorem smul_assoc {M N} [SMul M N] [SMul N α] [SMul M α] [IsScalarTower M N α] (x : M) (y : N) (z : α) :
    (x • y) • z = x • y • z :=
  IsScalarTower.smul_assoc x y z

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