`BookProof.ChapterSchurIrreducible.rangeClosure_invariant` {F m : V →L[ℂ] V} (hc : Commute F m) {w : V} (hw : w ∈ rangeClosure F) : m w ∈ rangeClosure F
ProvedBookProof.ChapterSchurIrreducible.rangeClosure_invarianttheoremstimepiece
Prove the following Lean 4 theorem from ChapterSchurIrreducible.
BookProof.ChapterSchurIrreducible.rangeClosure_invariant {F m : V →L[ℂ] V} (hc : Commute F m) {w : V} (hw : w ∈ rangeClosure F) : m w ∈ rangeClosure F
Formalization note: Lean 4 identifier BookProof.ChapterSchurIrreducible.rangeClosure_invariant.
Preamble
-- Generated from ChapterSchurIrreducible.lean — theorem BookProof.ChapterSchurIrreducible.rangeClosure_invariant
import Definitions.Def_ChapterA
import Mathlib
import Definitions.Def_ChapterSchurIrreducible
open BookProof.ChapterSchurIrreducible
open scoped ComplexConjugate InnerProductSpace
open BookProof.ChapterA BookProof.ChapterA.System
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V] [CompleteSpace V]Formal statement
theorem BookProof.ChapterSchurIrreducible.rangeClosure_invariant {F m : V →L[ℂ] V} (hc : Commute F m) {w : V}
(hw : w ∈ rangeClosure F) : m w ∈ rangeClosure F := by sorry