def Representation.IsUnitary {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (ρ : Representation 𝕜 G E) : Prop

A representation ρ on a finite-dimensional inner product space is unitary if ρ x is a unitary operator for each x.

Equations

• ρ.IsUnitary = ∀ (x : G), ρ x ∈ unitary (E →ₗ[𝕜] E)

@[simp]

theorem Representation.IsUnitary.trivial {𝕜 : Type u_1} {G : Type u_2} {E : Type u_3} [RCLike 𝕜] [Group G] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : (trivial 𝕜 G E).IsUnitary