English
Let x ∈ M and y ∈ N with N a monoid. Then (x • 1) * y = x • y; equivalently x acts diagonally on the product by distributing over multiplication.
Русский
Пусть x ∈ M и y ∈ N, где N — моноид. Тогда (x • 1) * y = x • y; то есть действие распределяется по умножению.
LaTeX
$$$ (x \cdot 1_N) \cdot y = x \cdot y $$$
Lean4
@[to_additive (attr := simp)]
theorem smul_one_mul {M N} [MulOneClass N] [SMul M N] [IsScalarTower M N N] (x : M) (y : N) : x • (1 : N) * y = x • y :=
by rw [smul_mul_assoc, one_mul]