mem_smul_span — Mathlib

English

For I an ideal and s a set of M, x ∈ I • span R s iff x ∈ span of all i b with i ∈ I and b ∈ s.

Русский

Для идеала I и множества s ⊆ M верно x ∈ I • span R s ↔ x ∈ span всех элементов i • b с i ∈ I, b ∈ s.

LaTeX

$$$x \\in I \\cdot \\operatorname{span} R s \\iff x \\in \\operatorname{span} \\big\\{ i \\cdot b \\;|\\; i \\in I,\\; b \\in s \\big\\}$$$

Lean4

theorem mem_smul_span {s : Set M} {x : M} :
    x ∈ I • Submodule.span R s ↔ x ∈ Submodule.span R (⋃ (a ∈ I) (b ∈ s), ({a • b} : Set M)) :=
  by
  rw [← I.span_eq, Submodule.span_smul_span, I.span_eq]
  simp

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