diff --git a/Mathlib/Algebra/Algebra/Unitization.lean b/Mathlib/Algebra/Algebra/Unitization.lean
index bcc514bc3823c..a56510dbb263b 100644
--- a/Mathlib/Algebra/Algebra/Unitization.lean
+++ b/Mathlib/Algebra/Algebra/Unitization.lean
@@ -578,8 +578,9 @@ instance instStarModule [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAdd
     [Module R A] [StarModule R A] : StarModule R (Unitization R A) where
   star_smul r x := ext (by simp) (by simp)
 
-instance instStarRing [CommSemiring R] [StarRing R] [NonUnitalSemiring A] [StarRing A] [Module R A]
-    [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] : StarRing (Unitization R A) :=
+instance instStarRing [CommSemiring R] [StarRing R] [NonUnitalNonAssocSemiring A] [StarRing A]
+    [Module R A] [StarModule R A] :
+    StarRing (Unitization R A) :=
   { Unitization.instStarAddMonoid with
     star_mul := fun x y =>
       ext (by simp [-star_mul']) (by simp [-star_mul', add_comm (star x.fst • star y.snd)]) }
diff --git a/Mathlib/Algebra/Star/Basic.lean b/Mathlib/Algebra/Star/Basic.lean
index bfd4ea0de5d70..e80068786d480 100644
--- a/Mathlib/Algebra/Star/Basic.lean
+++ b/Mathlib/Algebra/Star/Basic.lean
@@ -25,7 +25,7 @@ For now we simply do not introduce notations,
 as different users are expected to feel strongly about the relative merits of
 `r^*`, `r†`, `rᘁ`, and so on.
 
-Our star rings are actually star semirings, but of course we can prove
+Our star rings are actually star non-unital, non-associative, semirings, but of course we can prove
 `star_neg : star (-r) = - star r` when the underlying semiring is a ring.
 -/
 
@@ -121,21 +121,21 @@ export TrivialStar (star_trivial)
 
 attribute [simp] star_trivial
 
-/-- A `*`-semigroup is a semigroup `R` with an involutive operation `star`
+/-- A `*`-magma is a magma `R` with an involutive operation `star`
 such that `star (r * s) = star s * star r`.
 -/
-class StarSemigroup (R : Type u) [Semigroup R] extends InvolutiveStar R where
+class StarMul (R : Type u) [Mul R] extends InvolutiveStar R where
   /-- `star` skew-distributes over multiplication. -/
   star_mul : ∀ r s : R, star (r * s) = star s * star r
-#align star_semigroup StarSemigroup
+#align star_semigroup StarMul
 
-export StarSemigroup (star_mul)
+export StarMul (star_mul)
 
 attribute [simp 900] star_mul
 
-section StarSemigroup
+section StarMul
 
-variable [Semigroup R] [StarSemigroup R]
+variable [Mul R] [StarMul R]
 
 theorem star_star_mul (x y : R) : star (star x * y) = star y * x := by rw [star_mul, star_star]
 #align star_star_mul star_star_mul
@@ -164,17 +164,17 @@ theorem commute_star_comm {x y : R} : Commute (star x) y ↔ Commute x (star y)
   rw [← commute_star_star, star_star]
 #align commute_star_comm commute_star_comm
 
-end StarSemigroup
+end StarMul
 
 /-- In a commutative ring, make `simp` prefer leaving the order unchanged. -/
 @[simp]
-theorem star_mul' [CommSemigroup R] [StarSemigroup R] (x y : R) : star (x * y) = star x * star y :=
+theorem star_mul' [CommSemigroup R] [StarMul R] (x y : R) : star (x * y) = star x * star y :=
   (star_mul x y).trans (mul_comm _ _)
 #align star_mul' star_mul'
 
 /-- `star` as a `MulEquiv` from `R` to `Rᵐᵒᵖ` -/
 @[simps apply]
-def starMulEquiv [Semigroup R] [StarSemigroup R] : R ≃* Rᵐᵒᵖ :=
+def starMulEquiv [Mul R] [StarMul R] : R ≃* Rᵐᵒᵖ :=
   { (InvolutiveStar.star_involutive.toPerm star).trans opEquiv with
     toFun := fun x => MulOpposite.op (star x)
     map_mul' := fun x y => by simp only [star_mul, op_mul] }
@@ -183,7 +183,7 @@ def starMulEquiv [Semigroup R] [StarSemigroup R] : R ≃* Rᵐᵒᵖ :=
 
 /-- `star` as a `MulAut` for commutative `R`. -/
 @[simps apply]
-def starMulAut [CommSemigroup R] [StarSemigroup R] : MulAut R :=
+def starMulAut [CommSemigroup R] [StarMul R] : MulAut R :=
   { InvolutiveStar.star_involutive.toPerm star with
     toFun := star
     map_mul' := star_mul' }
@@ -193,32 +193,32 @@ def starMulAut [CommSemigroup R] [StarSemigroup R] : MulAut R :=
 variable (R)
 
 @[simp]
-theorem star_one [Monoid R] [StarSemigroup R] : star (1 : R) = 1 :=
+theorem star_one [MulOneClass R] [StarMul R] : star (1 : R) = 1 :=
   op_injective <| (starMulEquiv : R ≃* Rᵐᵒᵖ).map_one.trans (op_one _).symm
 #align star_one star_one
 
 variable {R}
 
 @[simp]
-theorem star_pow [Monoid R] [StarSemigroup R] (x : R) (n : ℕ) : star (x ^ n) = star x ^ n :=
+theorem star_pow [Monoid R] [StarMul R] (x : R) (n : ℕ) : star (x ^ n) = star x ^ n :=
   op_injective <|
     ((starMulEquiv : R ≃* Rᵐᵒᵖ).toMonoidHom.map_pow x n).trans (op_pow (star x) n).symm
 #align star_pow star_pow
 
 @[simp]
-theorem star_inv [Group R] [StarSemigroup R] (x : R) : star x⁻¹ = (star x)⁻¹ :=
+theorem star_inv [Group R] [StarMul R] (x : R) : star x⁻¹ = (star x)⁻¹ :=
   op_injective <| ((starMulEquiv : R ≃* Rᵐᵒᵖ).toMonoidHom.map_inv x).trans (op_inv (star x)).symm
 #align star_inv star_inv
 
 @[simp]
-theorem star_zpow [Group R] [StarSemigroup R] (x : R) (z : ℤ) : star (x ^ z) = star x ^ z :=
+theorem star_zpow [Group R] [StarMul R] (x : R) (z : ℤ) : star (x ^ z) = star x ^ z :=
   op_injective <|
     ((starMulEquiv : R ≃* Rᵐᵒᵖ).toMonoidHom.map_zpow x z).trans (op_zpow (star x) z).symm
 #align star_zpow star_zpow
 
 /-- When multiplication is commutative, `star` preserves division. -/
 @[simp]
-theorem star_div [CommGroup R] [StarSemigroup R] (x y : R) : star (x / y) = star x / star y :=
+theorem star_div [CommGroup R] [StarMul R] (x y : R) : star (x / y) = star x / star y :=
   map_div (starMulAut : R ≃* R) _ _
 #align star_div star_div
 
@@ -227,17 +227,17 @@ theorem star_div [CommGroup R] [StarSemigroup R] (x y : R) : star (x / y) = star
 See note [reducible non-instances].
 -/
 @[reducible]
-def starSemigroupOfComm {R : Type*} [CommMonoid R] : StarSemigroup R where
+def starMulOfComm {R : Type*} [CommMonoid R] : StarMul R where
   star := id
   star_involutive _ := rfl
   star_mul := mul_comm
-#align star_semigroup_of_comm starSemigroupOfComm
+#align star_semigroup_of_comm starMulOfComm
 
 section
 
-attribute [local instance] starSemigroupOfComm
+attribute [local instance] starMulOfComm
 
-/-- Note that since `starSemigroupOfComm` is reducible, `simp` can already prove this. -/
+/-- Note that since `starMulOfComm` is reducible, `simp` can already prove this. -/
 theorem star_id_of_comm {R : Type*} [CommSemiring R] {x : R} : star x = x :=
   rfl
 #align star_id_of_comm star_id_of_comm
@@ -302,35 +302,35 @@ theorem star_zsmul [AddGroup R] [StarAddMonoid R] (x : R) (n : ℤ) : star (n 
   (starAddEquiv : R ≃+ R).toAddMonoidHom.map_zsmul _ _
 #align star_zsmul star_zsmul
 
-/-- A `*`-ring `R` is a (semi)ring with an involutive `star` operation which is additive
-which makes `R` with its multiplicative structure into a `*`-semigroup
+/-- A `*`-ring `R` is a non-unital, non-associative (semi)ring with an involutive `star` operation
+which is additive which makes `R` with its multiplicative structure into a `*`-multiplication
 (i.e. `star (r * s) = star s * star r`).  -/
-class StarRing (R : Type u) [NonUnitalSemiring R] extends StarSemigroup R where
+class StarRing (R : Type u) [NonUnitalNonAssocSemiring R] extends StarMul R where
   /-- `star` commutes with addition -/
   star_add : ∀ r s : R, star (r + s) = star r + star s
 #align star_ring StarRing
 
-instance (priority := 100) StarRing.toStarAddMonoid [NonUnitalSemiring R] [StarRing R] :
+instance (priority := 100) StarRing.toStarAddMonoid [NonUnitalNonAssocSemiring R] [StarRing R] :
     StarAddMonoid R where
   star_add := StarRing.star_add
 #align star_ring.to_star_add_monoid StarRing.toStarAddMonoid
 
 /-- `star` as a `RingEquiv` from `R` to `Rᵐᵒᵖ` -/
 @[simps apply]
-def starRingEquiv [NonUnitalSemiring R] [StarRing R] : R ≃+* Rᵐᵒᵖ :=
+def starRingEquiv [NonUnitalNonAssocSemiring R] [StarRing R] : R ≃+* Rᵐᵒᵖ :=
   { starAddEquiv.trans (MulOpposite.opAddEquiv : R ≃+ Rᵐᵒᵖ), starMulEquiv with
     toFun := fun x => MulOpposite.op (star x) }
 #align star_ring_equiv starRingEquiv
 #align star_ring_equiv_apply starRingEquiv_apply
 
 @[simp, norm_cast]
-theorem star_natCast [Semiring R] [StarRing R] (n : ℕ) : star (n : R) = n :=
+theorem star_natCast [NonAssocSemiring R] [StarRing R] (n : ℕ) : star (n : R) = n :=
   (congr_arg unop (map_natCast (starRingEquiv : R ≃+* Rᵐᵒᵖ) n)).trans (unop_natCast _)
 #align star_nat_cast star_natCast
 
 --Porting note: new theorem
 @[simp]
-theorem star_ofNat [Semiring R] [StarRing R] (n : ℕ) [n.AtLeastTwo] :
+theorem star_ofNat [NonAssocSemiring R] [StarRing R] (n : ℕ) [n.AtLeastTwo] :
     star (no_index (OfNat.ofNat n) : R) = OfNat.ofNat n :=
   star_natCast _
 
@@ -459,7 +459,7 @@ See note [reducible non-instances].
 -/
 @[reducible]
 def starRingOfComm {R : Type*} [CommSemiring R] : StarRing R :=
-  { starSemigroupOfComm with
+  { starMulOfComm with
     star := id
     star_add := fun _ _ => rfl }
 #align star_ring_of_comm starRingOfComm
@@ -486,7 +486,7 @@ export StarModule (star_smul)
 attribute [simp] star_smul
 
 /-- A commutative star monoid is a star module over itself via `Monoid.toMulAction`. -/
-instance StarSemigroup.to_starModule [CommMonoid R] [StarSemigroup R] : StarModule R R :=
+instance StarSemigroup.to_starModule [CommMonoid R] [StarMul R] : StarModule R R :=
   ⟨star_mul'⟩
 #align star_semigroup.to_star_module StarSemigroup.to_starModule
 
@@ -517,9 +517,9 @@ end
 
 namespace Units
 
-variable [Monoid R] [StarSemigroup R]
+variable [Monoid R] [StarMul R]
 
-instance : StarSemigroup Rˣ where
+instance : StarMul Rˣ where
   star u :=
     { val := star u
       inv := star ↑u⁻¹
@@ -543,12 +543,12 @@ instance {A : Type*} [Star A] [SMul R A] [StarModule R A] : StarModule Rˣ A :=
 
 end Units
 
-theorem IsUnit.star [Monoid R] [StarSemigroup R] {a : R} : IsUnit a → IsUnit (star a)
+theorem IsUnit.star [Monoid R] [StarMul R] {a : R} : IsUnit a → IsUnit (star a)
   | ⟨u, hu⟩ => ⟨Star.star u, hu ▸ rfl⟩
 #align is_unit.star IsUnit.star
 
 @[simp]
-theorem isUnit_star [Monoid R] [StarSemigroup R] {a : R} : IsUnit (star a) ↔ IsUnit a :=
+theorem isUnit_star [Monoid R] [StarMul R] {a : R} : IsUnit (star a) ↔ IsUnit a :=
   ⟨fun h => star_star a ▸ h.star, IsUnit.star⟩
 #align is_unit_star isUnit_star
 
@@ -560,14 +560,14 @@ theorem Ring.inverse_star [Semiring R] [StarRing R] (a : R) :
   rw [Ring.inverse_non_unit _ ha, Ring.inverse_non_unit _ (mt isUnit_star.mp ha), star_zero]
 #align ring.inverse_star Ring.inverse_star
 
-instance Invertible.star {R : Type*} [Monoid R] [StarSemigroup R] (r : R) [Invertible r] :
+instance Invertible.star {R : Type*} [MulOneClass R] [StarMul R] (r : R) [Invertible r] :
     Invertible (star r) where
   invOf := Star.star (⅟ r)
   invOf_mul_self := by rw [← star_mul, mul_invOf_self, star_one]
   mul_invOf_self := by rw [← star_mul, invOf_mul_self, star_one]
 #align invertible.star Invertible.star
 
-theorem star_invOf {R : Type*} [Monoid R] [StarSemigroup R] (r : R) [Invertible r]
+theorem star_invOf {R : Type*} [Monoid R] [StarMul R] (r : R) [Invertible r]
     [Invertible (star r)] : star (⅟ r) = ⅟ (star r) := by
   have : star (⅟ r) = star (⅟ r) * ((star r) * ⅟ (star r)) := by
     simp only [mul_invOf_self, mul_one]
@@ -594,7 +594,7 @@ theorem op_star [Star R] (r : R) : op (star r) = star (op r) :=
 instance [InvolutiveStar R] : InvolutiveStar Rᵐᵒᵖ where
   star_involutive r := unop_injective (star_star r.unop)
 
-instance [Monoid R] [StarSemigroup R] : StarSemigroup Rᵐᵒᵖ where
+instance [Mul R] [StarMul R] : StarMul Rᵐᵒᵖ where
   star_mul x y := unop_injective (star_mul y.unop x.unop)
 
 instance [AddMonoid R] [StarAddMonoid R] : StarAddMonoid Rᵐᵒᵖ where
@@ -607,7 +607,7 @@ end MulOpposite
 
 /-- A commutative star monoid is a star module over its opposite via
 `Monoid.toOppositeMulAction`. -/
-instance StarSemigroup.toOpposite_starModule [CommMonoid R] [StarSemigroup R] :
+instance StarSemigroup.toOpposite_starModule [CommMonoid R] [StarMul R] :
     StarModule Rᵐᵒᵖ R :=
   ⟨fun r s => star_mul' s r.unop⟩
 #align star_semigroup.to_opposite_star_module StarSemigroup.toOpposite_starModule
diff --git a/Mathlib/Algebra/Star/BigOperators.lean b/Mathlib/Algebra/Star/BigOperators.lean
index a799e669fffec..70ec49b8ee77b 100644
--- a/Mathlib/Algebra/Star/BigOperators.lean
+++ b/Mathlib/Algebra/Star/BigOperators.lean
@@ -19,7 +19,7 @@ variable {R : Type*}
 open BigOperators
 
 @[simp]
-theorem star_prod [CommMonoid R] [StarSemigroup R] {α : Type*} (s : Finset α) (f : α → R) :
+theorem star_prod [CommMonoid R] [StarMul R] {α : Type*} (s : Finset α) (f : α → R) :
     star (∏ x in s, f x) = ∏ x in s, star (f x) := map_prod (starMulAut : R ≃* R) _ _
 #align star_prod star_prod
 
diff --git a/Mathlib/Algebra/Star/CHSH.lean b/Mathlib/Algebra/Star/CHSH.lean
index 99d0b4e402f30..6c43e8fc13e4d 100644
--- a/Mathlib/Algebra/Star/CHSH.lean
+++ b/Mathlib/Algebra/Star/CHSH.lean
@@ -82,7 +82,7 @@ The physical interpretation is that `A₀` and `A₁` are a pair of boolean obse
 are spacelike separated from another pair `B₀` and `B₁` of boolean observables.
 -/
 --@[nolint has_nonempty_instance] Porting note: linter does not exist
-structure IsCHSHTuple {R} [Monoid R] [StarSemigroup R] (A₀ A₁ B₀ B₁ : R) : Prop where
+structure IsCHSHTuple {R} [Monoid R] [StarMul R] (A₀ A₁ B₀ B₁ : R) : Prop where
   A₀_inv : A₀ ^ 2 = 1
   A₁_inv : A₁ ^ 2 = 1
   B₀_inv : B₀ ^ 2 = 1
diff --git a/Mathlib/Algebra/Star/Center.lean b/Mathlib/Algebra/Star/Center.lean
index 8148b6259c866..8ae164483c00d 100644
--- a/Mathlib/Algebra/Star/Center.lean
+++ b/Mathlib/Algebra/Star/Center.lean
@@ -10,7 +10,7 @@ import Mathlib.Algebra.Star.Pointwise
 
 /-! # `Set.center`, `Set.centralizer` and the `star` operation -/
 
-variable {R : Type*} [Semigroup R] [StarSemigroup R] {a : R} {s : Set R}
+variable {R : Type*} [Mul R] [StarMul R] {a : R} {s : Set R}
 
 theorem Set.star_mem_center (ha : a ∈ Set.center R) : star a ∈ Set.center R := by
   simpa only [star_mul, star_star] using fun g =>
diff --git a/Mathlib/Algebra/Star/Free.lean b/Mathlib/Algebra/Star/Free.lean
index 9fd8017cf96a3..6bee8b53463c4 100644
--- a/Mathlib/Algebra/Star/Free.lean
+++ b/Mathlib/Algebra/Star/Free.lean
@@ -23,7 +23,7 @@ namespace FreeMonoid
 
 variable {α : Type*}
 
-instance : StarSemigroup (FreeMonoid α) where
+instance : StarMul (FreeMonoid α) where
   star := List.reverse
   star_involutive := List.reverse_reverse
   star_mul := List.reverse_append
diff --git a/Mathlib/Algebra/Star/Module.lean b/Mathlib/Algebra/Star/Module.lean
index 594f29f3d492a..30f6c294b9901 100644
--- a/Mathlib/Algebra/Star/Module.lean
+++ b/Mathlib/Algebra/Star/Module.lean
@@ -82,7 +82,7 @@ def starLinearEquiv (R : Type*) {A : Type*} [CommSemiring R] [StarRing R] [AddCo
     map_smul' := star_smul }
 #align star_linear_equiv starLinearEquiv
 
-variable (R : Type*) (A : Type*) [Semiring R] [StarSemigroup R] [TrivialStar R] [AddCommGroup A]
+variable (R : Type*) (A : Type*) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A]
   [Module R A] [StarAddMonoid A] [StarModule R A]
 
 /-- The self-adjoint elements of a star module, as a submodule. -/
@@ -184,7 +184,7 @@ def StarModule.decomposeProdAdjoint : A ≃ₗ[R] selfAdjoint A × skewAdjoint A
 
 @[simp]
 theorem algebraMap_star_comm {R A : Type*} [CommSemiring R] [StarRing R] [Semiring A]
-    [StarSemigroup A] [Algebra R A] [StarModule R A] (r : R) :
+    [StarMul A] [Algebra R A] [StarModule R A] (r : R) :
     algebraMap R A (star r) = star (algebraMap R A r) := by
   simp only [Algebra.algebraMap_eq_smul_one, star_smul, star_one]
 #align algebra_map_star_comm algebraMap_star_comm
diff --git a/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean b/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
index 6bb33112b9dc0..00c9713bb7494 100644
--- a/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
+++ b/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
@@ -26,10 +26,11 @@ instance instInvolutiveStar {S R : Type*} [InvolutiveStar R] [SetLike S R] [Star
     (s : S) : InvolutiveStar s where
   star_involutive r := Subtype.ext <| star_star (r : R)
 
-/-- In a star semigroup (i.e., a semigroup with an antimultiplicative involutive star operation),
-any star-closed subset which is also closed under multiplication is itself a star semigroup. -/
-instance instStarSemigroup {S R : Type*} [Semigroup R] [StarSemigroup R] [SetLike S R]
-    [MulMemClass S R] [StarMemClass S R] (s : S) : StarSemigroup s where
+/-- In a star magma (i.e., a multiplication with an antimultiplicative involutive star
+operation), any star-closed subset which is also closed under multiplication is itself a star
+magma. -/
+instance instStarMul {S R : Type*} [Mul R] [StarMul R] [SetLike S R]
+    [MulMemClass S R] [StarMemClass S R] (s : S) : StarMul s where
   star_mul _ _ := Subtype.ext <| star_mul _ _
 
 /-- In a `StarAddMonoid` (i.e., an additive monoid with an additive involutive star operation), any
@@ -39,11 +40,12 @@ instance instStarAddMonoid {S R : Type*} [AddMonoid R] [StarAddMonoid R] [SetLik
     [AddSubmonoidClass S R] [StarMemClass S R] (s : S) : StarAddMonoid s where
   star_add _ _ := Subtype.ext <| star_add _ _
 
-/-- In a star ring (i.e., a non-unital semiring with an additive, antimultiplicative, involutive
-star operation), an star-closed non-unital subsemiring is itself a star ring. -/
-instance instStarRing {S R : Type*} [NonUnitalSemiring R] [StarRing R] [SetLike S R]
+/-- In a star ring (i.e., a non-unital, non-associative, semiring with an additive,
+antimultiplicative, involutive star operation), a star-closed non-unital subsemiring is itself a
+star ring. -/
+instance instStarRing {S R : Type*} [NonUnitalNonAssocSemiring R] [StarRing R] [SetLike S R]
     [NonUnitalSubsemiringClass S R] [StarMemClass S R] (s : S) : StarRing s :=
-  { StarMemClass.instStarSemigroup s, StarMemClass.instStarAddMonoid s with }
+  { StarMemClass.instStarMul s, StarMemClass.instStarAddMonoid s with }
 
 /-- In a star `R`-module (i.e., `star (r • m) = (star r) • m`) any star-closed subset which is also
 closed under the scalar action by `R` is itself a star `R`-module. -/
diff --git a/Mathlib/Algebra/Star/Pi.lean b/Mathlib/Algebra/Star/Pi.lean
index 751458b2f8b1f..6d92e8e94b26c 100644
--- a/Mathlib/Algebra/Star/Pi.lean
+++ b/Mathlib/Algebra/Star/Pi.lean
@@ -43,7 +43,7 @@ instance [∀ i, Star (f i)] [∀ i, TrivialStar (f i)] : TrivialStar (∀ i, f
 instance [∀ i, InvolutiveStar (f i)] : InvolutiveStar (∀ i, f i)
     where star_involutive _ := funext fun _ => star_star _
 
-instance [∀ i, Semigroup (f i)] [∀ i, StarSemigroup (f i)] : StarSemigroup (∀ i, f i)
+instance [∀ i, Mul (f i)] [∀ i, StarMul (f i)] : StarMul (∀ i, f i)
     where star_mul _ _ := funext fun _ => star_mul _ _
 
 instance [∀ i, AddMonoid (f i)] [∀ i, StarAddMonoid (f i)] : StarAddMonoid (∀ i, f i)
diff --git a/Mathlib/Algebra/Star/Pointwise.lean b/Mathlib/Algebra/Star/Pointwise.lean
index 3c4338543181b..c6cf5251618f4 100644
--- a/Mathlib/Algebra/Star/Pointwise.lean
+++ b/Mathlib/Algebra/Star/Pointwise.lean
@@ -117,7 +117,7 @@ theorem star_singleton {β : Type*} [InvolutiveStar β] (x : β) : ({x} : Set β
   rw [mem_star, mem_singleton_iff, mem_singleton_iff, star_eq_iff_star_eq, eq_comm]
 #align set.star_singleton Set.star_singleton
 
-protected theorem star_mul [Monoid α] [StarSemigroup α] (s t : Set α) : (s * t)⋆ = t⋆ * s⋆ := by
+protected theorem star_mul [Mul α] [StarMul α] (s t : Set α) : (s * t)⋆ = t⋆ * s⋆ := by
  simp_rw [← image_star, ← image2_mul, image_image2, image2_image_left, image2_image_right,
    star_mul, image2_swap _ s t]
 #align set.star_mul Set.star_mul
@@ -134,7 +134,7 @@ instance [Star α] [TrivialStar α] : TrivialStar (Set α) where
     ext1
     simp [star_trivial]
 
-protected theorem star_inv [Group α] [StarSemigroup α] (s : Set α) : s⁻¹⋆ = s⋆⁻¹ := by
+protected theorem star_inv [Group α] [StarMul α] (s : Set α) : s⁻¹⋆ = s⋆⁻¹ := by
   ext
   simp only [mem_star, mem_inv, star_inv]
 #align set.star_inv Set.star_inv
diff --git a/Mathlib/Algebra/Star/Prod.lean b/Mathlib/Algebra/Star/Prod.lean
index 04c11726814a0..89d1cdc7dc4e5 100644
--- a/Mathlib/Algebra/Star/Prod.lean
+++ b/Mathlib/Algebra/Star/Prod.lean
@@ -44,15 +44,16 @@ instance [Star R] [Star S] [TrivialStar R] [TrivialStar S] : TrivialStar (R × S
 instance [InvolutiveStar R] [InvolutiveStar S] : InvolutiveStar (R × S)
     where star_involutive _ := Prod.ext (star_star _) (star_star _)
 
-instance [Semigroup R] [Semigroup S] [StarSemigroup R] [StarSemigroup S] : StarSemigroup (R × S)
+instance [Mul R] [Mul S] [StarMul R] [StarMul S] : StarMul (R × S)
     where star_mul _ _ := Prod.ext (star_mul _ _) (star_mul _ _)
 
 instance [AddMonoid R] [AddMonoid S] [StarAddMonoid R] [StarAddMonoid S] : StarAddMonoid (R × S)
     where star_add _ _ := Prod.ext (star_add _ _) (star_add _ _)
 
-instance [NonUnitalSemiring R] [NonUnitalSemiring S] [StarRing R] [StarRing S] : StarRing (R × S) :=
+instance [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [StarRing R] [StarRing S] :
+    StarRing (R × S) :=
   { inferInstanceAs (StarAddMonoid (R × S)),
-    inferInstanceAs (StarSemigroup (R × S)) with }
+    inferInstanceAs (StarMul (R × S)) with }
 
 instance {α : Type w} [SMul α R] [SMul α S] [Star α] [Star R] [Star S]
     [StarModule α R] [StarModule α S] : StarModule α (R × S)
@@ -61,7 +62,7 @@ instance {α : Type w} [SMul α R] [SMul α S] [Star α] [Star R] [Star S]
 end Prod
 
 --Porting note: removing @[simp], `simp` simplifies LHS
-theorem Units.embed_product_star [Monoid R] [StarSemigroup R] (u : Rˣ) :
+theorem Units.embed_product_star [Monoid R] [StarMul R] (u : Rˣ) :
     Units.embedProduct R (star u) = star (Units.embedProduct R u) :=
   rfl
 #align units.embed_product_star Units.embed_product_star
diff --git a/Mathlib/Algebra/Star/SelfAdjoint.lean b/Mathlib/Algebra/Star/SelfAdjoint.lean
index 28a6b5a5478d5..e1c0b5ba3b63b 100644
--- a/Mathlib/Algebra/Star/SelfAdjoint.lean
+++ b/Mathlib/Algebra/Star/SelfAdjoint.lean
@@ -82,12 +82,12 @@ theorem star_iff [InvolutiveStar R] {x : R} : IsSelfAdjoint (star x) ↔ IsSelfA
 #align is_self_adjoint.star_iff IsSelfAdjoint.star_iff
 
 @[simp]
-theorem star_mul_self [Semigroup R] [StarSemigroup R] (x : R) : IsSelfAdjoint (star x * x) := by
+theorem star_mul_self [Mul R] [StarMul R] (x : R) : IsSelfAdjoint (star x * x) := by
   simp only [IsSelfAdjoint, star_mul, star_star]
 #align is_self_adjoint.star_mul_self IsSelfAdjoint.star_mul_self
 
 @[simp]
-theorem mul_star_self [Semigroup R] [StarSemigroup R] (x : R) : IsSelfAdjoint (x * star x) := by
+theorem mul_star_self [Mul R] [StarMul R] (x : R) : IsSelfAdjoint (x * star x) := by
   simpa only [star_star] using star_mul_self (star x)
 #align is_self_adjoint.mul_star_self IsSelfAdjoint.mul_star_self
 
@@ -157,7 +157,7 @@ end AddCommMonoid
 
 section Semigroup
 
-variable [Semigroup R] [StarSemigroup R]
+variable [Semigroup R] [StarMul R]
 
 theorem conjugate {x : R} (hx : IsSelfAdjoint x) (z : R) : IsSelfAdjoint (z * x * star z) := by
   simp only [isSelfAdjoint_iff, star_mul, star_star, mul_assoc, hx.star_eq]
@@ -173,9 +173,9 @@ theorem isStarNormal {x : R} (hx : IsSelfAdjoint x) : IsStarNormal x :=
 
 end Semigroup
 
-section Monoid
+section MulOneClass
 
-variable [Monoid R] [StarSemigroup R]
+variable [MulOneClass R] [StarMul R]
 
 variable (R)
 
@@ -183,7 +183,11 @@ theorem _root_.isSelfAdjoint_one : IsSelfAdjoint (1 : R) :=
   star_one R
 #align is_self_adjoint_one isSelfAdjoint_one
 
-variable {R}
+end MulOneClass
+
+section Monoid
+
+variable [Monoid R] [StarMul R]
 
 theorem pow {x : R} (hx : IsSelfAdjoint x) (n : ℕ) : IsSelfAdjoint (x ^ n) := by
   simp only [isSelfAdjoint_iff, star_pow, hx.star_eq]
@@ -210,7 +214,7 @@ end Semiring
 
 section CommSemigroup
 
-variable [CommSemigroup R] [StarSemigroup R]
+variable [CommSemigroup R] [StarMul R]
 
 theorem mul {x y : R} (hx : IsSelfAdjoint x) (hy : IsSelfAdjoint y) : IsSelfAdjoint (x * y) := by
   simp only [isSelfAdjoint_iff, star_mul', hx.star_eq, hy.star_eq]
@@ -561,23 +565,23 @@ instance isStarNormal_zero [Semiring R] [StarRing R] : IsStarNormal (0 : R) :=
   ⟨by simp only [Commute.refl, star_comm_self, star_zero]⟩
 #align is_star_normal_zero isStarNormal_zero
 
-instance isStarNormal_one [Monoid R] [StarSemigroup R] : IsStarNormal (1 : R) :=
+instance isStarNormal_one [MulOneClass R] [StarMul R] : IsStarNormal (1 : R) :=
   ⟨by simp only [Commute.refl, star_comm_self, star_one]⟩
 #align is_star_normal_one isStarNormal_one
 
-instance isStarNormal_star_self [Monoid R] [StarSemigroup R] {x : R} [IsStarNormal x] :
+instance isStarNormal_star_self [Mul R] [StarMul R] {x : R} [IsStarNormal x] :
     IsStarNormal (star x) :=
   ⟨show star (star x) * star x = star x * star (star x) by rw [star_star, star_comm_self']⟩
 #align is_star_normal_star_self isStarNormal_star_self
 
 -- see Note [lower instance priority]
-instance (priority := 100) TrivialStar.isStarNormal [Monoid R] [StarSemigroup R] [TrivialStar R]
+instance (priority := 100) TrivialStar.isStarNormal [Mul R] [StarMul R] [TrivialStar R]
     {x : R} : IsStarNormal x :=
   ⟨by rw [star_trivial]⟩
 #align has_trivial_star.is_star_normal TrivialStar.isStarNormal
 
 -- see Note [lower instance priority]
-instance (priority := 100) CommMonoid.isStarNormal [CommMonoid R] [StarSemigroup R] {x : R} :
+instance (priority := 100) CommMonoid.isStarNormal [CommMonoid R] [StarMul R] {x : R} :
     IsStarNormal x :=
   ⟨mul_comm _ _⟩
 #align comm_monoid.is_star_normal CommMonoid.isStarNormal
diff --git a/Mathlib/Algebra/Star/Unitary.lean b/Mathlib/Algebra/Star/Unitary.lean
index 795362afca5d2..d6215a6484f4c 100644
--- a/Mathlib/Algebra/Star/Unitary.lean
+++ b/Mathlib/Algebra/Star/Unitary.lean
@@ -26,7 +26,7 @@ unitary
 /-- In a *-monoid, `unitary R` is the submonoid consisting of all the elements `U` of
 `R` such that `star U * U = 1` and `U * star U = 1`.
 -/
-def unitary (R : Type*) [Monoid R] [StarSemigroup R] : Submonoid R where
+def unitary (R : Type*) [Monoid R] [StarMul R] : Submonoid R where
   carrier := { U | star U * U = 1 ∧ U * star U = 1 }
   one_mem' := by simp only [mul_one, and_self_iff, Set.mem_setOf_eq, star_one]
   mul_mem' := @fun U B ⟨hA₁, hA₂⟩ ⟨hB₁, hB₂⟩ => by
@@ -47,7 +47,7 @@ namespace unitary
 
 section Monoid
 
-variable [Monoid R] [StarSemigroup R]
+variable [Monoid R] [StarMul R]
 
 theorem mem_iff {U : R} : U ∈ unitary R ↔ star U * U = 1 ∧ U * star U = 1 :=
   Iff.rfl
@@ -109,7 +109,7 @@ instance : InvolutiveStar (unitary R) :=
     ext
     rw [coe_star, coe_star, star_star]⟩
 
-instance : StarSemigroup (unitary R) :=
+instance : StarMul (unitary R) :=
   ⟨by
     intro x y
     ext
@@ -143,7 +143,7 @@ end Monoid
 
 section CommMonoid
 
-variable [CommMonoid R] [StarSemigroup R]
+variable [CommMonoid R] [StarMul R]
 
 instance : CommGroup (unitary R) :=
   { inferInstanceAs (Group (unitary R)), Submonoid.toCommMonoid _ with }
@@ -160,7 +160,7 @@ end CommMonoid
 
 section GroupWithZero
 
-variable [GroupWithZero R] [StarSemigroup R]
+variable [GroupWithZero R] [StarMul R]
 
 @[norm_cast]
 theorem coe_inv (U : unitary R) : ↑U⁻¹ = (U⁻¹ : R) :=
diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean
index 63d61fe56d14c..686fa8c35044a 100644
--- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean
@@ -204,7 +204,7 @@ instance : Star (E →L[𝕜] E) :=
 instance : InvolutiveStar (E →L[𝕜] E) :=
   ⟨adjoint_adjoint⟩
 
-instance : StarSemigroup (E →L[𝕜] E) :=
+instance : StarMul (E →L[𝕜] E) :=
   ⟨adjoint_comp⟩
 
 instance : StarRing (E →L[𝕜] E) :=
@@ -455,7 +455,7 @@ instance : Star (E →ₗ[𝕜] E) :=
 instance : InvolutiveStar (E →ₗ[𝕜] E) :=
   ⟨adjoint_adjoint⟩
 
-instance : StarSemigroup (E →ₗ[𝕜] E) :=
+instance : StarMul (E →ₗ[𝕜] E) :=
   ⟨adjoint_comp⟩
 
 instance : StarRing (E →ₗ[𝕜] E) :=
diff --git a/Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean b/Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean
index c587bb1ea3101..0ff228a39b066 100644
--- a/Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean
+++ b/Mathlib/Analysis/NormedSpace/Star/GelfandDuality.lean
@@ -149,7 +149,7 @@ theorem gelfandTransform_isometry : Isometry (gelfandTransform ℂ A) := by
     roots shows that the norm is preserved. -/
   have : spectralRadius ℂ (gelfandTransform ℂ A (star a * a)) = spectralRadius ℂ (star a * a) := by
     unfold spectralRadius; rw [spectrum.gelfandTransform_eq]
-  rw [map_mul, (IsSelfAdjoint.star_mul_self _).spectralRadius_eq_nnnorm, gelfandTransform_map_star,
+  rw [map_mul, (IsSelfAdjoint.star_mul_self a).spectralRadius_eq_nnnorm, gelfandTransform_map_star,
     (IsSelfAdjoint.star_mul_self (gelfandTransform ℂ A a)).spectralRadius_eq_nnnorm] at this
   simp only [ENNReal.coe_eq_coe, CstarRing.nnnorm_star_mul_self, ← sq] at this
   simpa only [Function.comp_apply, NNReal.sqrt_sq] using
diff --git a/Mathlib/Data/Matrix/Basic.lean b/Mathlib/Data/Matrix/Basic.lean
index 0d3e51527708c..db995af1c4bb0 100644
--- a/Mathlib/Data/Matrix/Basic.lean
+++ b/Mathlib/Data/Matrix/Basic.lean
@@ -2210,7 +2210,7 @@ theorem conjTranspose_smul_non_comm [Star R] [Star α] [SMul R α] [SMul Rᵐᵒ
 #align matrix.conj_transpose_smul_non_comm Matrix.conjTranspose_smul_non_comm
 
 -- @[simp] -- Porting note: simp can prove this
-theorem conjTranspose_smul_self [Semigroup α] [StarSemigroup α] (c : α) (M : Matrix m n α) :
+theorem conjTranspose_smul_self [Mul α] [StarMul α] (c : α) (M : Matrix m n α) :
     (c • M)ᴴ = MulOpposite.op (star c) • Mᴴ :=
   conjTranspose_smul_non_comm c M star_mul
 #align matrix.conj_transpose_smul_self Matrix.conjTranspose_smul_self
diff --git a/Mathlib/Topology/Algebra/Module/Star.lean b/Mathlib/Topology/Algebra/Module/Star.lean
index 112221949ea72..2263e97759417 100644
--- a/Mathlib/Topology/Algebra/Module/Star.lean
+++ b/Mathlib/Topology/Algebra/Module/Star.lean
@@ -44,7 +44,7 @@ def starL' (R : Type*) {A : Type*} [CommSemiring R] [StarRing R] [TrivialStar R]
       A ≃L⋆[R] A)
 #align starL' starL'
 
-variable (R : Type*) (A : Type*) [Semiring R] [StarSemigroup R] [TrivialStar R] [AddCommGroup A]
+variable (R : Type*) (A : Type*) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A]
   [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible (2 : R)] [TopologicalSpace A]
 
 theorem continuous_selfAdjointPart [ContinuousAdd A] [ContinuousStar A] [ContinuousConstSMul R A] :
diff --git a/Mathlib/Topology/Algebra/Star.lean b/Mathlib/Topology/Algebra/Star.lean
index ade667268ab6b..11ec313906f1f 100644
--- a/Mathlib/Topology/Algebra/Star.lean
+++ b/Mathlib/Topology/Algebra/Star.lean
@@ -95,7 +95,7 @@ instance {C : ι → Type*} [∀ i, TopologicalSpace (C i)] [∀ i, Star (C i)]
 instance [Star R] [TopologicalSpace R] [ContinuousStar R] : ContinuousStar Rᵐᵒᵖ :=
   ⟨MulOpposite.continuous_op.comp <| MulOpposite.continuous_unop.star⟩
 
-instance [Monoid R] [StarSemigroup R] [TopologicalSpace R] [ContinuousStar R] :
+instance [Monoid R] [StarMul R] [TopologicalSpace R] [ContinuousStar R] :
     ContinuousStar Rˣ :=
   ⟨continuous_induced_rng.2 Units.continuous_embedProduct.star⟩
 
diff --git a/Mathlib/Topology/ContinuousFunction/Algebra.lean b/Mathlib/Topology/ContinuousFunction/Algebra.lean
index 0a7ef04a18a72..771d9f1060209 100644
--- a/Mathlib/Topology/ContinuousFunction/Algebra.lean
+++ b/Mathlib/Topology/ContinuousFunction/Algebra.lean
@@ -970,13 +970,13 @@ instance starAddMonoid [AddMonoid β] [ContinuousAdd β] [StarAddMonoid β] [Con
     StarAddMonoid C(α, β) where
   star_add _ _ := ext fun _ => star_add _ _
 
-instance starSemigroup [Semigroup β] [ContinuousMul β] [StarSemigroup β] [ContinuousStar β] :
-    StarSemigroup C(α, β) where
+instance starMul [Mul β] [ContinuousMul β] [StarMul β] [ContinuousStar β] :
+    StarMul C(α, β) where
   star_mul _ _ := ext fun _ => star_mul _ _
 
-instance [NonUnitalSemiring β] [TopologicalSemiring β] [StarRing β] [ContinuousStar β] :
+instance [NonUnitalNonAssocSemiring β] [TopologicalSemiring β] [StarRing β] [ContinuousStar β] :
     StarRing C(α, β) :=
-  { ContinuousMap.starAddMonoid, ContinuousMap.starSemigroup with }
+  { ContinuousMap.starAddMonoid, ContinuousMap.starMul with }
 
 instance [Star R] [Star β] [SMul R β] [StarModule R β] [ContinuousStar β]
     [ContinuousConstSMul R β] : StarModule R C(α, β) where