span_le_restrictScalars — Mathlib

English

If f maps s into t, then f maps span(s) into span(t).

Русский

Если отображение f переводит s в t, то оно переводит span(s) в span(t).

LaTeX

$$$\text{MapsTo}(f,s,t) \Rightarrow \text{MapsTo}(f,\operatorname{span}(s),\operatorname{span}(t))$$$

Lean4

/-- If `R` is "smaller" ring than `S` then the span by `R` is smaller than the span by `S`. -/
theorem span_le_restrictScalars : span R s ≤ (span S s).restrictScalars R :=
  Submodule.span_le.2 Submodule.subset_span

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