`BookProof.ChapterWeylSL2Group.coeff_mem_of_poly_mem` {W : Submodule ℂ V} {N : ℕ} {c : ℕ → V} (h : ∀ t : ℂ, ∑ k ∈ Finset.range N, t ^ k • c k ∈ W) {k : ℕ} (hk : k < N) : c...
ProvedBookProof.ChapterWeylSL2Group.coeff_mem_of_poly_memtheoremstimepiece
Prove the following Lean 4 theorem from ChapterWeylSL2Group.
BookProof.ChapterWeylSL2Group.coeff_mem_of_poly_mem {W : Submodule ℂ V} {N : ℕ} {c : ℕ → V} (h : ∀ t : ℂ, ∑ k ∈ Finset.range N, t ^ k • c k ∈ W) {k : ℕ} (hk : k < N) : c k ∈ W
Formalization note: Lean 4 identifier BookProof.ChapterWeylSL2Group.coeff_mem_of_poly_mem.
Preamble
-- Generated from ChapterWeylSL2Group.lean — theorem BookProof.ChapterWeylSL2Group.coeff_mem_of_poly_mem
import Definitions.Def_ChapterWeylSl2
import Mathlib
import Definitions.Def_ChapterWeylSL2Group
open BookProof.ChapterWeylSL2Group
open BookProof.ChapterWeylSl2
universe u
variable {V : Type u} [AddCommGroup V] [Module ℂ V]Formal statement
theorem BookProof.ChapterWeylSL2Group.coeff_mem_of_poly_mem {W : Submodule ℂ V} {N : ℕ} {c : ℕ → V}
(h : ∀ t : ℂ, ∑ k ∈ Finset.range N, t ^ k • c k ∈ W) {k : ℕ} (hk : k < N) : c k ∈ W := by sorry