small things

set.mm

@@ -649896,16 +649896,15 @@ fixed reference functional determined by this vector (corresponding to
 $)
 
 
-  $c AlgClosure $. $( Algebraic closure $)
+  $c AlgCl $. $( Algebraic closure $)
 
-  $( Integral elements of a ring. $)
-  calgclosure $a class AlgClosure $.
+  calgcl $a class AlgCl $.
 
   ${
     $d k l p z f q x $.
     $( Define the algebraic closure of any field.  (Contributed by metakunt,
        11-Jan-2025.) $)
-    df-algclosure $a |- AlgClosure = ( k e. Field |-> { l e. Field |
+    df-algcl $a |- AlgCl = ( k e. Field |-> { l e. Field |
       ( A. p e. ( Base ` ( Poly1 ` l ) ) ( ( deg1 ` p ) e. NN ->
       E. z e. ( Base ` l ) ( ( ( eval1 ` l ) ` p ) ` z ) = ( 0g ` l ) ) /\
       E. f e. ( k RingHom l ) A. x e. l E. q e. ( Base ` ( Poly1 ` k ) )
@@ -649916,7 +649915,7 @@ fixed reference functional determined by this vector (corresponding to
   ${
     $( The algebraic closure exists for any field.  We are sadly nowhere near
        of proving that yet.  (Contributed by metakunt, 11-Jan-2025.) $)
-    ax-algclex $a |- ( K e. Field -> ( AlgClosure ` K ) =/= (/) ) $.
+    ax-algclex $a |- ( K e. Field -> ( AlgCl ` K ) =/= (/) ) $.
   $}
 
 $(