smul_subset_smul — Mathlib

English

The set-version of smul distributes over submodule product: (↑I : Set A) • (↑N : Set M) ⊆ (↑(I • N) : Set M).

Русский

Множество-версия smul распределяется по произведению подмодулов: (↑I : Set A) • (↑N : Set M) ⊆ (↑(I • N) : Set M).

LaTeX

$$$ (\uparrow I : \text{Set } A) \cdot (\uparrow N : \text{Set } M) \subseteq \uparrow (I \cdot N) $$$

Lean4

theorem smul_subset_smul : (↑I : Set A) • (↑N : Set M) ⊆ (↑(I • N) : Set M) :=
  AddSubmonoid.smul_subset_smul

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