mem_of_span_top_of_smul_mem — Mathlib

English

If M' is a submodule of M, s ⊆ R with span(s) = ⊤, and for all r ∈ s we have r•x ∈ M', then x ∈ M'.

Русский

Если M' ⊆ M и s ⊆ R таково, что span(s) = ⊤, и для каждого r ∈ s выполняется r•x ∈ M', то x ∈ M'.

LaTeX

$$span(s) = ⊤ ∧ (∀ r ∈ s, r • x ∈ M') ⇒ x ∈ M'$$

Lean4

theorem mem_of_span_top_of_smul_mem (M' : Submodule R M) (s : Set R) (hs : Ideal.span s = ⊤) (x : M)
    (H : ∀ r : s, (r : R) • x ∈ M') : x ∈ M' :=
  by
  suffices LinearMap.range (LinearMap.toSpanSingleton R M x) ≤ M'
    by
    rw [← LinearMap.toSpanSingleton_one R M x]
    exact this (LinearMap.mem_range_self _ 1)
  rw [LinearMap.range_eq_map, ← hs, map_le_iff_le_comap, Ideal.span, span_le]
  exact fun r hr ↦ H ⟨r, hr⟩

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