feat(Algebra/Star/StarRingHom): Add non-unital star ring homomorphisms (#12924)

Definitions and basic properties of  non-unital star ring homomorphisms



Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com>
Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>

Author: mans0954

Mathlib.lean

@@ -715,6 +715,7 @@ import Mathlib.Algebra.Star.Pointwise
 import Mathlib.Algebra.Star.Prod
 import Mathlib.Algebra.Star.SelfAdjoint
 import Mathlib.Algebra.Star.StarAlgHom
+import Mathlib.Algebra.Star.StarRingHom
 import Mathlib.Algebra.Star.Subalgebra
 import Mathlib.Algebra.Star.Unitary
 import Mathlib.Algebra.Symmetrized

Mathlib/Algebra/Star/StarAlgHom.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.Algebra.Equiv
 import Mathlib.Algebra.Algebra.NonUnitalHom
 import Mathlib.Algebra.Algebra.Prod
 import Mathlib.Algebra.Star.Prod
+import Mathlib.Algebra.Star.StarRingHom
 
 #align_import algebra.star.star_alg_hom from "leanprover-community/mathlib"@"35882ddc66524b6980532a123a4ad4166db34c81"
 
@@ -89,6 +90,9 @@ def toNonUnitalStarAlgHom [NonUnitalStarAlgHomClass F R A B] (f : F) : A →⋆
 instance [NonUnitalStarAlgHomClass F R A B] : CoeTC F (A →⋆ₙₐ[R] B) :=
   ⟨toNonUnitalStarAlgHom⟩
 
+instance [NonUnitalStarAlgHomClass F R A B] : NonUnitalStarRingHomClass F A B :=
+  NonUnitalStarRingHomClass.mk
+
 end NonUnitalStarAlgHomClass
 
 namespace NonUnitalStarAlgHom