feat: add two basic lemmas about selfAdjoint elements (#5169)

- `selfAdjoint` elements are automatically normal
- the image of an element under a star-preserving map in a space with a `TrivialStar` is self-adjoint

Mathlib/Algebra/Star/SelfAdjoint.lean

@@ -100,6 +100,12 @@ theorem starHom_apply {F R S : Type _} [Star R] [Star S] [StarHomClass F R S] {x
   show star (f x) = f x from map_star f x ▸ congr_arg f hx
 #align is_self_adjoint.star_hom_apply IsSelfAdjoint.starHom_apply
 
+/- note: this lemma is *not* marked as `simp` so that Lean doesn't look for a `[TrivialStar R]`
+instance every time it sees `⊢ IsSelfAdjoint (f x)`, which will likely occur relatively often. -/
+theorem _root_.isSelfAdjoint_starHom_apply {F R S : Type _} [Star R] [Star S] [StarHomClass F R S]
+    [TrivialStar R] (f : F) (x : R) : IsSelfAdjoint (f x) :=
+  (IsSelfAdjoint.all x).starHom_apply f
+
 section AddMonoid
 
 variable [AddMonoid R] [StarAddMonoid R]
@@ -314,6 +320,10 @@ instance : Inhabited (selfAdjoint R) :=
 
 end AddGroup
 
+instance isStarNormal [NonUnitalRing R] [StarRing R] (x : selfAdjoint R) :
+    IsStarNormal (x : R) :=
+  x.prop.isStarNormal
+
 section Ring
 
 variable [Ring R] [StarRing R]