theorem Submodule.list_prod_mem_pow {R : Type u_1} [Semiring R] {A : Type u_2} [Semiring A] [Module R A] [IsScalarTower R A A] (M : Submodule R A) (n : ℕ) (l : List A) (hl : l.length = n) (hlM : ∀ x ∈ l, x ∈ M) : l.prod ∈ M ^ n

theorem Submodule.mul_def_noncomm {R : Type u_1} [Semiring R] {A : Type u_2} [Semiring A] [Module R A] [IsScalarTower R A A] (M N : Submodule R A) : M * N = span R (↑M * ↑N)

theorem Submodule.span_mul {R : Type u_1} [Semiring R] {A : Type u_2} [Semiring A] [Module R A] [IsScalarTower R A A] (T : Set A) (M : Submodule R A) : span R T * M = span R (T * ↑M)

theorem Submodule.pow_eq_span_pow_set_noncomm {R : Type u_1} [Semiring R] {A : Type u_2} [Semiring A] [Module R A] [IsScalarTower R A A] (M : Submodule R A) (n : ℕ) : M ^ n = span R (↑M ^ n)

theorem Submodule.mul_span {R : Type u_3} [CommSemiring R] {A : Type u_4} [Semiring A] [Algebra R A] (M : Submodule R A) (S : Set A) : M * span R S = span R (↑M * S)