pointwiseSetSMul — Mathlib

English

If m ∈ S, then a · m ∈ a · S; i.e., smul preserves membership at the element level.

Русский

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

LaTeX

$$$m \\in S \\rightarrow a \\cdot m \\in a \\cdot S$$$

Lean4

/-- Let `s ⊆ R` be a set and `N ≤ M` be a submodule, then `s • N` is the smallest submodule containing
all `r • n` where `r ∈ s` and `n ∈ N`.
-/
protected def pointwiseSetSMul : SMul (Set S) (Submodule R M) where
  smul s N := sInf {p | ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p}

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