smul_def — Mathlib

English

For any SMul action of the ambient ring R on α, the action of a subring element s ∈ S on α agrees with the ambient action.

Русский

Для любого действия SMul кольца R на α, действие элемента подкольца s на α совпадает с общим действием.

LaTeX

$$$ \\forall [SMul R α], \\; (g : S) (m : α), g \\cdot m = (g : R) \\cdot m $$$

Lean4

theorem smul_def [SMul R α] {S : Subring R} (g : S) (m : α) : g • m = (g : R) • m :=
  rfl

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