smul_mem_pointwise_smul — Mathlib

English

If m ∈ S, then a · m ∈ a · S; i.e., smul preserves membership via pointwise action.

Русский

Если m ∈ S, то a · m ∈ a · S; т.е. действие сохраняет принадлежность по точечному умножению.

LaTeX

$$$m \\in S \\ \\Rightarrow \\ a \\cdot m \\in a \\cdot S$$$

Lean4

theorem smul_mem_pointwise_smul (m : M) (a : α) (S : Submodule R M) : m ∈ S → a • m ∈ a • S :=
  (Set.smul_mem_smul_set : _ → _ ∈ a • (S : Set M))

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