chore: rename StarSemigroup.to_starModule (#8994)

leanprover-community · Dec 19, 2023 · 0966330 · 0966330
1 parent 88a85a5
commit 0966330
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Mathlib/Algebra/Star/Basic.lean b/Mathlib/Algebra/Star/Basic.lean
@@ -488,9 +488,9 @@ 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] [StarMul R] : StarModule R R :=
+instance StarMul.toStarModule [CommMonoid R] [StarMul R] : StarModule R R :=
   ⟨star_mul'⟩
-#align star_semigroup.to_star_module StarSemigroup.to_starModule
+#align star_semigroup.to_star_module StarMul.toStarModule
 
 namespace RingHomInvPair