`BookProof.ChapterUnitaryCompleteReducibility.exists_irreducible_invariant_le` [FiniteDimensional ℂ V] {ρ : G →* (V ≃ₗᵢ[ℂ] V)} {U : Submodule ℂ V} (hU : IsInvariant ρ U) (hUne : U
ProvedBookProof.ChapterUnitaryCompleteReducibility.exists_irreducible_invariant_letheoremstimepiece
Prove the following Lean 4 theorem from ChapterUnitaryCompleteReducibility.
BookProof.ChapterUnitaryCompleteReducibility.exists_irreducible_invariant_le [FiniteDimensional ℂ V] {ρ : G →* (V ≃ₗᵢ[ℂ] V)} {U : Submodule ℂ V} (hU : IsInvariant ρ U) (hUne : U ≠ ⊥) : ∃ W ≤ U, IsIrreducibleInvariant ρ W
Formalization note: Lean 4 identifier BookProof.ChapterUnitaryCompleteReducibility.exists_irreducible_invariant_le.
Preamble
-- Generated from ChapterUnitaryCompleteReducibility.lean — theorem BookProof.ChapterUnitaryCompleteReducibility.exists_irreducible_invariant_le
import Mathlib
import Definitions.Def_ChapterUnitaryCompleteReducibility
import Definitions.Def_ChapterMaschkeFiniteGroup
open BookProof.ChapterMaschkeFiniteGroup
open BookProof.ChapterUnitaryCompleteReducibility
open Submodule
variable {G : Type*} [Group G] {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℂ V]Formal statement
theorem BookProof.ChapterUnitaryCompleteReducibility.exists_irreducible_invariant_le [FiniteDimensional ℂ V]
{ρ : G →* (V ≃ₗᵢ[ℂ] V)} {U : Submodule ℂ V} (hU : IsInvariant ρ U) (hUne : U ≠ ⊥) :
∃ W ≤ U, IsIrreducibleInvariant ρ W := by sorry