smul_pi_subset — Mathlib

English

For a family of modules R i with scalars from K, and a subset S of indices with t i ⊆ R i, the scalar action satisfies r • pi_s t ⊆ pi_s (r • t).

Русский

Для семейства модулей R_i со скалярами из K и подмножеством индексов S с t_i ⊆ R_i скалярное действие удовлетворяет равенству r • π_S t ⊆ π_S (r • t).

LaTeX

$$$r \\cdot (\\pi_s t) \\subseteq \\pi_s (r \\cdot t).$$$

Lean4

@[to_additive]
theorem smul_pi_subset [∀ i, SMul K (R i)] (r : K) (s : Set ι) (t : ∀ i, Set (R i)) : r • pi s t ⊆ pi s (r • t) :=
  piMap_image_pi_subset _

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