Theorems · Definition · linear algebra

LinearMap.toSpanSingleton

(R : Type u_1) →
  (M : Type u_4) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M → R →ₗ[R] M

Given an element x of a module M over R, the natural map from R to scalar multiples of x. See also LinearMap.ringLmapEquivSelf.

Defined in

Mathlib.LinearAlgebra.Span.Basic

Cited by

78 results in Mathlib

Foundations

Depth 25 from the axioms · uses no axioms

Assumes

SemiringAddCommMonoidModule