smul_one_smul — Mathlib

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]

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