mem_of_span_eq_top_of_smul_pow_mem

English

For any N, (⊤ : Ideal R) • N = N.

Русский

Для любого N: (⊤ : Ideal R) • N = N.

LaTeX

$$$(\\top : Ideal R) \\cdot N = N$$$

Lean4

/-- Given `s`, a generating set of `R`, to check that an `x : M` falls in a
submodule `M'` of `x`, we only need to show that `r ^ n • x ∈ M'` for some `n` for each `r : s`. -/
theorem mem_of_span_eq_top_of_smul_pow_mem (M' : Submodule R M) (s : Set R) (hs : Ideal.span s = ⊤) (x : M)
    (H : ∀ r : s, ∃ n : ℕ, ((r : R) ^ n : R) • x ∈ M') : x ∈ M' :=
  by
  choose f hf using H
  apply M'.mem_of_span_top_of_smul_mem _ (Ideal.span_range_pow_eq_top s hs f)
  rintro ⟨_, r, hr, rfl⟩
  exact hf r

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