Theorems · Theorem · commutative algebra

Submodule.mem_of_span_eq_top_of_smul_pow_mem

∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (M' : Submodule R M) (s : Set R), Ideal.span s = ⊤ → ∀ (x : M), (∀ (r : ↑s), ∃ n, ↑r ^ n • x ∈ M') → x ∈ M'

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.

Defined in

Mathlib.RingTheory.Ideal.Operations

Cited by

6 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidModule