refactor(Mathlib/Algebra/Algebra/NonUnitalHom): reorder notations t…

…o prevent `A →ₙₐ[R] B` being delaborated as `A →ₛₙₐ[MonoidHom.id R] B` (#12762)
leanprover-community · May 12, 2024 · 61580db · 61580db
1 parent ce418e4
commit 61580db
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Mathlib/Algebra/Algebra/NonUnitalHom.lean b/Mathlib/Algebra/Algebra/NonUnitalHom.lean
@@ -59,10 +59,10 @@ structure NonUnitalAlgHom [Monoid R] [Monoid S] (φ : R →* S) (A : Type v) (B
 infixr:25 " →ₙₐ " => NonUnitalAlgHom _
 
 @[inherit_doc]
-notation:25 A " →ₙₐ[" R "] " B => NonUnitalAlgHom (MonoidHom.id R) A B
+notation:25 A " →ₛₙₐ[" φ "] " B => NonUnitalAlgHom φ A B
 
 @[inherit_doc]
-notation:25 A " →ₛₙₐ[" φ "] " B => NonUnitalAlgHom φ A B
+notation:25 A " →ₙₐ[" R "] " B => NonUnitalAlgHom (MonoidHom.id R) A B
 
 attribute [nolint docBlame] NonUnitalAlgHom.toMulHom