[rename] algebra scalars function -> algebra scalar lifting function

Author: zwang123

set.mm

@@ -283995,7 +283995,7 @@ the same dimension over the same (nonzero) ring.  (Contributed by AV,
   $( Algebraic span function. $)
   casp $a class AlgSpan $.
 
-  $( Class of algebra scalars function. $)
+  $( Class of algebra scalar lifting function. $)
   cascl $a class algSc $.
 
   ${
@@ -284407,8 +284407,8 @@ the same dimension over the same (nonzero) ring.  (Contributed by AV,
     asclfval.k $e |- K = ( Base ` F ) $.
     asclfval.s $e |- .x. = ( .s ` W ) $.
     asclfval.o $e |- .1. = ( 1r ` W ) $.
-    $( Function value of the algebra scalars function.  (Contributed by Mario
-       Carneiro, 8-Mar-2015.) $)
+    $( Function value of the algebra scalar lifting function.  (Contributed by
+       Mario Carneiro, 8-Mar-2015.) $)
     asclfval $p |- A = ( x e. K |-> ( x .x. .1. ) ) $=
       ( vw cascl cfv cmpt cbs csca eqtr4di c0 cv cvv wcel wceq cur cvsca fveq2d
       co fveq2 eqidd oveq123d mpteq12dv df-ascl mptfvmpt wn mpt0 eqtrid mpteq1d
@@ -284430,7 +284430,7 @@ the same dimension over the same (nonzero) ring.  (Contributed by AV,
     asclfn.a $e |- A = ( algSc ` W ) $.
     asclfn.f $e |- F = ( Scalar ` W ) $.
     asclfn.k $e |- K = ( Base ` F ) $.
-    $( Unconditional functionality of the algebra scalars function.
+    $( Unconditional functionality of the algebra scalar lifting function.
        (Contributed by Mario Carneiro, 9-Mar-2015.) $)
     asclfn $p |- A Fn K $=
       ( vx cv cur cfv cvsca co ovex eqid asclfval fnmpti ) HCHIZDJKZDLKZMARSTNH
@@ -284446,7 +284446,7 @@ the same dimension over the same (nonzero) ring.  (Contributed by AV,
     ${
       asclf.k $e |- K = ( Base ` F ) $.
       asclf.b $e |- B = ( Base ` W ) $.
-      $( The algebra scalars function is a function into the base set.
+      $( The algebra scalar lifting function is a function into the base set.
          (Contributed by Mario Carneiro, 4-Jul-2015.) $)
       asclf $p |- ( ph -> A : K --> B ) $=
         ( vx cv cur cfv cvsca wcel adantr eqid co clmod simpr ringidcl lmodvscl
@@ -284455,8 +284455,8 @@ the same dimension over the same (nonzero) ring.  (Contributed by AV,
         NUMDEFGHKUTUSUJUK $.
     $}
 
-    $( The algebra scalars function is a group homomorphism.  (Contributed by
-       Mario Carneiro, 4-Jul-2015.) $)
+    $( The algebra scalar lifting function is a group homomorphism.
+       (Contributed by Mario Carneiro, 4-Jul-2015.) $)
     asclghm $p |- ( ph -> A e. ( F GrpHom W ) ) $=
       ( vx vy cplusg cfv cbs eqid crg wcel syl co wceq asclval lmodring ringgrp
       clmod asclf cv cur cvsca adantr simprl simprr ringidcl lmodvsdir syl13anc
@@ -284529,7 +284529,7 @@ the same dimension over the same (nonzero) ring.  (Contributed by AV,
     ascldimul.k $e |- K = ( Base ` F ) $.
     ascldimul.t $e |- .X. = ( .r ` W ) $.
     ascldimul.s $e |- .x. = ( .r ` F ) $.
-    $( The algebra scalars function distributes over multiplication.
+    $( The algebra scalar lifting function distributes over multiplication.
        (Contributed by Mario Carneiro, 8-Mar-2015.)  (Proof shortened by SN,
        5-Nov-2023.) $)
     ascldimul $p |- ( ( W e. AssAlg /\ R e. K /\ S e. K ) ->
@@ -284564,8 +284564,8 @@ the same dimension over the same (nonzero) ring.  (Contributed by AV,
     $d x y A $.  $d x y F $.  $d x y W $.
     asclrhm.a $e |- A = ( algSc ` W ) $.
     asclrhm.f $e |- F = ( Scalar ` W ) $.
-    $( The algebra scalars function is a ring homomorphism.  (Contributed by
-       Mario Carneiro, 8-Mar-2015.) $)
+    $( The algebra scalar lifting function is a ring homomorphism.
+       (Contributed by Mario Carneiro, 8-Mar-2015.) $)
     asclrhm $p |- ( W e. AssAlg -> A e. ( F RingHom W ) ) $=
       ( vx vy casa wcel cbs cfv cmulr cur assasca assaring assalmod ascl1 cv co
       eqid wceq ascldimul 3expb asclghm isrhm2d ) CHIZFGBJKZBCBLKZCLKZBMKZACMKZ
@@ -292258,7 +292258,7 @@ series in the subring which are also polynomials (in the parent ring).
           ( crg wcel cid cfv ply1sca2 ply1ring ply1lmod cbs cnx baseid strfvi
           asclf ) DJKABDLMECGCDFNCDFOCDFPDQRQMESHTIUA $.
 
-        $( The value of the algebra scalars function for (univariate)
+        $( The value of the algebra scalar lifting function for (univariate)
            polynomials applied to a scalar results in a constant polynomial.
            (Contributed by AV, 27-Nov-2019.) $)
         ply1sclcl $p |- ( ( R e. Ring /\ S e. K ) -> ( A ` S ) e. B ) $=
@@ -301895,8 +301895,9 @@ are univariate (or multivariate) polynomials. See Wikipedia "Polynomial
     pmat0opsc.z $e |- .0. = ( 0g ` R ) $.
     $( The zero polynomial matrix over a ring represented as operation with
        "lifted scalars" (i.e. elements of the ring underlying the polynomial
-       ring embedded into the polynomial ring by the scalar injection/algebraic
-       scalars function ` algSc ` ).  (Contributed by AV, 16-Nov-2019.) $)
+       ring embedded into the polynomial ring by the scalar injection/algebra
+       scalar lifting function ` algSc ` ).  (Contributed by AV,
+       16-Nov-2019.) $)
     pmat0opsc $p |- ( ( N e. Fin /\ R e. Ring )
                       -> ( 0g ` C ) = ( i e. N , j e. N |-> ( A ` .0. ) ) ) $=
       ( cfn wcel crg wa c0g cfv cmpo eqid pmat0op wceq ply1scl0 eqcomd mpoeq3dv
@@ -835256,8 +835257,8 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
     ${
       $d A x $.  $d C x $.  $d M x $.  $d W x $.  $d ph x $.
       asclcntr.m $e |- M = ( mulGrp ` W ) $.
-      $( The algebra scalars function maps into the center of the algebra.
-         Equivalently, a lifted scalar is a center of the algebra.
+      $( The algebra scalar lifting function maps into the center of the
+         algebra.  Equivalently, a lifted scalar is a center of the algebra.
          (Contributed by Zhi Wang, 11-Sep-2025.) $)
       asclcntr $p |- ( ph -> ( A ` C ) e. ( Cntr ` M ) ) $=
         ( vx cbs cfv eqid wcel co adantr ccntr asclelbas cv wa casa cmulr simpr
@@ -835280,7 +835281,7 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
          a "vector" element of ` W ` , of the "scalar" ` C ` , which is now an
          upper triangular matrix, with the "vector" ` X e. ( Base `` W ) ` .
 
-         Equivalently, the algebra scalars function is not necessarily
+         Equivalently, the algebra scalar lifting function is not necessarily
          injective unless the algebra is faithful.  Therefore, all "scalar
          injection" was renamed.