mem_set_smul_def — Mathlib

English

The operation s • N for a set s of scalars is defined as the infimum of all submodules containing every r · n with r ∈ s and n ∈ N.

Русский

Операция s • N определяется как Inf над всеми подмодулями, содержащими каждое r · n, где r ∈ s и n ∈ N.

LaTeX

$$$\\mathrm{pointwiseSetSMul}(s, N) = \\bigcap_{p:\\ Submodule\\ R\\ M\\, (\\forall r\\in s, n\\in N, r\\cdot n\\in p)} p$$$

Lean4

theorem mem_set_smul_def (x : M) :
    x ∈ s • N ↔ x ∈ sInf {p : Submodule R M | ∀ ⦃r : S⦄ {n : M}, r ∈ s → n ∈ N → r • n ∈ p} :=
  Iff.rfl

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