From 9a775482ed3da38c311245ce476f52af36a9753e Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Mon, 11 Dec 2023 23:03:27 -0600 Subject: [PATCH] chore: rename `StarSemigroup.to_starModule` --- Mathlib/Algebra/Star/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Star/Basic.lean b/Mathlib/Algebra/Star/Basic.lean index 6ba1b26626cd9..b139858543a93 100644 --- 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