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