`BookProof.ChapterMaschkeFiniteGroup.maschke_invariant_complement` [Finite G] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) (W : Submodule ℂ V) (hW : IsInvariant ρ W) : ∃ W' :
ProvedBookProof.ChapterMaschkeFiniteGroup.maschke_invariant_complementtheoremstimepiece
Prove the following Lean 4 theorem from ChapterMaschkeFiniteGroup.
BookProof.ChapterMaschkeFiniteGroup.maschke_invariant_complement [Finite G] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) (W : Submodule ℂ V) (hW : IsInvariant ρ W) : ∃ W' : Submodule ℂ V, IsInvariant ρ W' ∧ IsCompl W W'
Formalization note: Lean 4 identifier BookProof.ChapterMaschkeFiniteGroup.maschke_invariant_complement.
Preamble
-- Generated from ChapterMaschkeFiniteGroup.lean — theorem BookProof.ChapterMaschkeFiniteGroup.maschke_invariant_complement
import Mathlib
import Definitions.Def_ChapterMaschkeFiniteGroup
open BookProof.ChapterMaschkeFiniteGroup
variable {G : Type*} [Group G] {V : Type*} [AddCommGroup V] [Module ℂ V]Formal statement
theorem BookProof.ChapterMaschkeFiniteGroup.maschke_invariant_complement [Finite G] [FiniteDimensional ℂ V]
(ρ : Representation ℂ G V) (W : Submodule ℂ V) (hW : IsInvariant ρ W) :
∃ W' : Submodule ℂ V, IsInvariant ρ W' ∧ IsCompl W W' := by sorry