`BookProof.ChapterUnitaryCompleteReducibility.isInvariant_top` (ρ : G →* (V ≃ₗᵢ[ℂ] V)) : IsInvariant ρ (⊤ : Submodule ℂ V)
ProvedBookProof.ChapterUnitaryCompleteReducibility.isInvariant_toptheoremstimepiece
Prove the following Lean 4 theorem from ChapterUnitaryCompleteReducibility.
BookProof.ChapterUnitaryCompleteReducibility.isInvariant_top (ρ : G →* (V ≃ₗᵢ[ℂ] V)) : IsInvariant ρ (⊤ : Submodule ℂ V)
Formalization note: Lean 4 identifier BookProof.ChapterUnitaryCompleteReducibility.isInvariant_top.
Preamble
-- Generated from ChapterUnitaryCompleteReducibility.lean — theorem BookProof.ChapterUnitaryCompleteReducibility.isInvariant_top
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.isInvariant_top (ρ : G →* (V ≃ₗᵢ[ℂ] V)) : IsInvariant ρ (⊤ : Submodule ℂ V) := by sorry