`BookProof.ChapterWeylSL2Group.pow_mem_of_mem` {W : Submodule ℂ V} {a : Module.End ℂ V} (ha : ∀ x ∈ W, a x ∈ W) {v : V} (hv : v ∈ W) (k : ℕ) : (a ^ k) v ∈ W

Initializing...

`BookProof.ChapterWeylSL2Group.pow_mem_of_mem` {W : Submodule ℂ V} {a : Module.End ℂ V} (ha : ∀ x ∈ W, a x ∈ W) {v : V} (hv : v ∈ W) (k : ℕ) : (a ^ k) v ∈ W · Prove2Me