smul_mem_span_smul_of_mem — Mathlib

English

A symmetric form of the above span equality under surjective algebra map.

Русский

Симметричная форма равенства порождённых оболочек при сюръективном отображении алгебры.

LaTeX

$$$$\\text{surjective} \\Rightarrow (\\operatorname{Submodule.cast}\\ldots)$$$$

Lean4

theorem smul_mem_span_smul_of_mem {s : Set S} {t : Set A} {k : S} (hks : k ∈ span R s) {x : A} (hx : x ∈ t) :
    k • x ∈ span R (s • t) :=
  span_induction (fun _ hc => subset_span <| Set.smul_mem_smul hc hx) (by rw [zero_smul]; exact zero_mem _)
    (fun c₁ c₂ _ _ ih₁ ih₂ => by rw [add_smul]; exact add_mem ih₁ ih₂)
    (fun b c _ hc => by rw [IsScalarTower.smul_assoc]; exact smul_mem _ _ hc) hks

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