feat(Algebra/Star/StarProjection): add IsStarProjection.map (#35898)

and attribute `IsStarProjection.{isIdempotentElem, isSelfAdjoint}` with `aesop` and `grind`.

Author: themathqueen

Mathlib/Algebra/Star/StarProjection.lean

@@ -28,6 +28,9 @@ structure IsStarProjection [Mul R] [Star R] (p : R) : Prop where
   protected isIdempotentElem : IsIdempotentElem p
   protected isSelfAdjoint : IsSelfAdjoint p
 
+attribute [grind →, aesop safe forward]
+  IsStarProjection.isIdempotentElem IsStarProjection.isSelfAdjoint
+
 namespace IsStarProjection
 
 variable {p q : R}
@@ -40,6 +43,12 @@ theorem isStarNormal [Mul R] [Star R]
     (hp : IsStarProjection p) : IsStarNormal p :=
   hp.isSelfAdjoint.isStarNormal
 
+protected theorem map {A B : Type*} [Mul A] [Star A] [Mul B] [Star B]
+    {F : Type*} [FunLike F A B] [StarHomClass F A B] [MulHomClass F A B]
+    {x : A} (hx : IsStarProjection x) (f : F) : IsStarProjection (f x) where
+  isIdempotentElem := hx.isIdempotentElem.map f
+  isSelfAdjoint := hx.isSelfAdjoint.map f
+
 variable (R) in
 @[simp]
 protected theorem zero [NonUnitalNonAssocSemiring R] [StarAddMonoid R] : IsStarProjection (0 : R) :=