diff --git a/Mathlib/LinearAlgebra/Matrix/ConjTranspose.lean b/Mathlib/LinearAlgebra/Matrix/ConjTranspose.lean index 5c730990d2ca34..6acd1c31f97c1d 100644 --- a/Mathlib/LinearAlgebra/Matrix/ConjTranspose.lean +++ b/Mathlib/LinearAlgebra/Matrix/ConjTranspose.lean @@ -424,14 +424,11 @@ instance [Star α] [Star β] [SMul α β] [StarModule α β] : StarModule α (Ma star_smul := conjTranspose_smul /-- When `α` is a \*-(semi)ring, `Matrix.star` is also a \*-(semi)ring. -/ -instance [Fintype n] [NonUnitalSemiring α] [StarRing α] : StarRing (Matrix n n α) where +instance [Fintype n] [NonUnitalNonAssocSemiring α] [StarRing α] : StarRing (Matrix n n α) where star_add := conjTranspose_add star_mul := conjTranspose_mul -/-- A version of `star_mul` for `*` instead of `*`. -/ -theorem star_mul [Fintype n] [NonUnitalNonAssocSemiring α] [StarRing α] (M N : Matrix n n α) : - star (M * N) = star N * star M := - conjTranspose_mul _ _ +@[deprecated (since := "2026-04-20")] protected alias star_mul := StarMul.star_mul end Star