smul_mem_span_smul' — Mathlib

English

If span_R s = ⊤, then for any t, span_R (s • t) equals the restricted span (span_S t).

Русский

Если span_R s = ⊤, то span_R (s • t) = (span_S t).restrictScalars.

LaTeX

$$$$\\operatorname{span}_R(s) = \\top \\Rightarrow \\operatorname{span}_R(s \\cdot t) = (\\operatorname{span}_S t).\\text{restrictScalars}(R)$$$$

Lean4

theorem smul_mem_span_smul' {s : Set S} (hs : span R s = ⊤) {t : Set A} {k : S} {x : A} (hx : x ∈ span R (s • t)) :
    k • x ∈ span R (s • t) := by rw [span_smul_of_span_eq_top hs] at hx ⊢; exact (span S t).smul_mem k hx

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