From e514bec43823fdb7335f5c4c51cdaf14876cbbb1 Mon Sep 17 00:00:00 2001 From: Christopher Hoskin Date: Thu, 9 May 2024 06:12:53 +0100 Subject: [PATCH] =?UTF-8?q?Deduce=20that=20Subsemiring.center=20(CentroidH?= =?UTF-8?q?om=20=CE=B1)=20is=20InvolutiveStar?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/Algebra/Ring/CentroidHom.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Ring/CentroidHom.lean b/Mathlib/Algebra/Ring/CentroidHom.lean index f79043168b452..7f599b4493fb7 100644 --- 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. -/