feat: add StarMemClass.coe_star (#9762)

leanprover-community · Jan 15, 2024 · 9007a3c · 9007a3c
1 parent 6e66ddc
commit 9007a3c
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/Mathlib/Algebra/Star/Basic.lean b/Mathlib/Algebra/Star/Basic.lean
@@ -71,6 +71,8 @@ variable {S : Type w} [Star R] [SetLike S R] [hS : StarMemClass S R] (s : S)
 instance instStar : Star s where
   star r := ⟨star (r : R), star_mem r.prop⟩
 
+@[simp] lemma coe_star (x : s) : star x = star (x : R) := rfl
+
 end StarMemClass
 
 /-- Typeclass for a star operation with is involutive.