toSpanSingleton — Mathlib

English

The natural map from R to the span of x, sending r to r·x, is linear.

Русский

Естественное отображение из кольца R в спан{x}, отправляющее r↦r·x, является линейным.

LaTeX

$$$toSpanSingleton\,x: R \to R\!\cdot x,\; r \mapsto r x$$$

Lean4

/-- Given an element `x` of a module `M` over `R`, the natural map from
`R` to scalar multiples of `x`. See also `LinearMap.ringLmapEquivSelf`. -/
@[simps!]
def toSpanSingleton (x : M) : R →ₗ[R] M :=
  LinearMap.id.smulRight x

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