Style fix: useless <|

leanprover-community · Dec 2, 2024 · 23a2d80 · 23a2d80
1 parent eee740b
commit 23a2d80
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/RingTheory/AlgebraicIndependent/Defs.lean b/Mathlib/RingTheory/AlgebraicIndependent/Defs.lean
@@ -141,7 +141,7 @@ theorem aeval_repr (p) : aeval x (hx.repr p) = p :=
   Subtype.ext_iff.1 (AlgEquiv.apply_symm_apply hx.aevalEquiv p)
 
 theorem aeval_comp_repr : (aeval x).comp hx.repr = Subalgebra.val _ :=
-  AlgHom.ext <| hx.aeval_repr
+  AlgHom.ext hx.aeval_repr
 
 end repr