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