English
Let x ∈ M and y ∈ α. Then (x • (1 : N)) • y = x • y; i.e., acting by the identity element has no effect.
Русский
Пусть x ∈ M и y ∈ α. Тогда (x • 1_N) • y = x • y; то есть действие единицы не изменяет элемент.
LaTeX
$$$ (x \cdot 1) \cdot y = x \cdot y $$$
Lean4
@[to_additive]
theorem smul_one_smul {M} (N) [Monoid N] [SMul M N] [MulAction N α] [SMul M α] [IsScalarTower M N α] (x : M) (y : α) :
(x • (1 : N)) • y = x • y := by rw [smul_assoc, one_smul]