coe_smul — Mathlib

English

Scalar multiplication is preserved under inclusion: the image of r·x equals r times the image of x, for r in R', x in S.

Русский

Умножение на скаляр сохраняется при включении: образ r·x равен r умножению на образ x, для r ∈ R', x ∈ S.

LaTeX

$$$ (r' \\cdot x)^{\\uparrow} = r' \\cdot (x^{\\uparrow}) \\quad (r' \\in R',\\ x \\in S). $$$

Lean4

@[simp, norm_cast]
theorem coe_smul [SMul R' R] [SMul R' A] [IsScalarTower R' R A] (r : R') (x : S) : ↑(r • x) = r • (x : A) :=
  rfl

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