Deduce that Subsemiring.center (CentroidHom α) is InvolutiveStar

leanprover-community · May 9, 2024 · e514bec · e514bec
1 parent 5859d83
commit e514bec
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/Mathlib/Algebra/Ring/CentroidHom.lean b/Mathlib/Algebra/Ring/CentroidHom.lean
@@ -698,7 +698,7 @@ instance : Star (CentroidHom α) where
 
 @[simp] lemma star_apply (f : CentroidHom α) (a : α) : (star f) a = star (f (star a)) := rfl
 
-instance : InvolutiveStar (CentroidHom α) where
+instance instInvolutiveStar : InvolutiveStar (CentroidHom α) where
   star_involutive _ := by
     ext a
     rw [star_apply, star_apply, star_star, star_star]
@@ -735,6 +735,9 @@ instance : Star (Subsemiring.center (CentroidHom α)) where
         _ = g (star (f.val (star a))) := by simp only [star_apply, star_star]
     exact e1.symm⟩
 
+instance : InvolutiveStar (Subsemiring.center (CentroidHom α)) where
+  star_involutive f := SetCoe.ext (instInvolutiveStar.star_involutive f.val)
+
 /--
 Let `α` be a star ring with commutative centroid. Then the centroid is a star ring.
 -/