smul_left — Mathlib

English

If x is an additive unit, then s • x is an additive unit for any s.

Русский

Если x является элементом-единицей по сложению, то для любого s элемент s • x также является элементом-единицей.

LaTeX

$$$\\forall S, M\\ [\\text{DistribSMul } S M],\\ IsAddUnit\\, x \\Rightarrow \\forall s\\in S,\n IsAddUnit (s \\cdot x)$$$

Lean4

theorem smul_left [DistribSMul S M] (hx : IsAddUnit x) (s : S) : IsAddUnit (s • x) :=
  hx.map (DistribSMul.toAddMonoidHom M s)

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