smul_one_mul — Mathlib

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]

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