structure FinDimRep (G : Type u_1) [Group G] (V : Type u_2) [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] : Type (max u_1 u_2)

• toMonoidHom : G →* V →ₗ[ℂ] V

def FinDimRep.IsIrreducible {G : Type u_1} [Group G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (π : FinDimRep G V) : Prop

theorem schur_scalar_finiteDim {G : Type u_1} [Group G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] [Nontrivial V] (π : FinDimRep G V) (hirr : π.IsIrreducible) (T : V →ₗ[ℂ] V) (hT : ∀ (g : G), T ∘ₗ π.toMonoidHom g = π.toMonoidHom g ∘ₗ T) : ∃ (c : ℂ), T = c • LinearMap.id

theorem schur_zero_or_iso_continuous {G : Type u_1} [Group G] [TopologicalSpace G] {V₁ : Type u_2} [AddCommGroup V₁] [Module ℂ V₁] [TopologicalSpace V₁] {V₂ : Type u_3} [AddCommGroup V₂] [Module ℂ V₂] [TopologicalSpace V₂] (π₁ : ContinuousRep G V₁) (π₂ : ContinuousRep G V₂) (hirr₁ : π₁.IsIrreducible) (hirr₂ : π₂.IsIrreducible) (T : RepHom π₁ π₂) : T.toContinuousLinearMap = 0 ∨ Function.Bijective ⇑T.toContinuousLinearMap

theorem schur_scalar_topological {G : Type u_1} [Group G] [TopologicalSpace G] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (π : ContinuousRep G E) (hirr : π.IsIrreducible) (T : RepHom π π) : ∃ (c : ℂ), T.toContinuousLinearMap = c • ContinuousLinearMap.id ℂ E