@[reducible, inline]

abbrev UnitaryRepresentation (𝕜 : Type u_1) (G : Type u_2) (E : Type u_3) [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : Type (max u_3 u_2)

Equations

• UnitaryRepresentation 𝕜 G E = (G →* E ≃ₗᵢ[𝕜] E)

noncomputable def UnitaryRepresentation.toRepresentation {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (ρ : UnitaryRepresentation 𝕜 G E) : Representation 𝕜 G E

Equations

• ρ.toRepresentation = { toFun := fun (g : G) => ↑↑↑(ρ g), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem UnitaryRepresentation.toRepresentation_apply {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (ρ : UnitaryRepresentation 𝕜 G E) (g : G) : ρ.toRepresentation g = ↑↑↑(ρ g)

@[reducible, inline]

abbrev UnitaryRepresentation.trivial (𝕜 : Type u_1) (G : Type u_2) (E : Type u_3) [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : UnitaryRepresentation 𝕜 G E

Equations

• UnitaryRepresentation.trivial 𝕜 G E = 1

theorem UnitaryRepresentation.finrank_eq_one_of_isIrreducible {G : Type u_2} {E : Type u_3} [CommGroup G] [NormedAddCommGroup E] [InnerProductSpace ℂ E] {ρ : UnitaryRepresentation ℂ G E} (hρ : ρ.toRepresentation.IsIrreducible) : Module.finrank ℂ E = 1