@[simp]

theorem LinearMap.id_mem_unitary {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : id ∈ unitary (E →ₗ[𝕜] E)