From 17f31c34a72f614196b081c5b05c8ece59c2dba8 Mon Sep 17 00:00:00 2001 From: Thierry Arnoux <5831830+tirix@users.noreply.github.com> Date: Fri, 17 Jan 2025 00:50:58 +0100 Subject: [PATCH 01/12] Constructible numbers - initial idea --- constr.mm | 139 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 139 insertions(+) create mode 100644 constr.mm diff --git a/constr.mm b/constr.mm new file mode 100644 index 0000000000..99c2145416 --- /dev/null +++ b/constr.mm @@ -0,0 +1,139 @@ +$[ set.mm $] + +$( +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# + Contructible numbers +#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# + This section defines the set of constructible points as complex numbers which + can be drawn starting from two points (we take ` 0 ` and ` 1 ` ), and taking + intersections of circles and lines. + + We initially define two sets: + + + We then proceed by showing that those two sets are equal. + + This construction is useful for proving the impossibility of doubling the + cube ( ~ imp2cube ), and of angle trisection ( ~ imp3ang ) +$) + + +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Degree of a field extension +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + ${ + fldextdgirred.b $e |- B = ( Base ` F ) $. + fldextdgirred.0 $e |- .0. = ( 0g ` F ) $. + fldextdgirred.d $e |- D = ( deg1 ` F ) $. + fldextdgirred.o $e |- O = ( eval1 ` F ) $. + fldextdgirred.m $e |- M = ( Poly1 ` F ) $. + fldextdgirred.k $e |- K = ( F |`s E ) $. + fldextdgirred.l $e |- L = ( F |`s ( F fldGen ( E u. { Z } ) ) ) $. + fldextdgirred.f $e |- ( ph -> F e. Field ) $. + fldextdgirred.e $e |- ( ph -> E e. ( SubDRing ` F ) ) $. + fldextdgirred.p $e |- ( ph -> P e. ( Base ` M ) ) $. + fldextdgirred.1 $e |- ( ph -> P e. ( Irred ` M ) ) $. + fldextdgirred.z $e |- ( ph -> Z e. ( B \ E ) ) $. + fldextdgirred.2 $e |- ( ph -> ( ( O ` P ) ` Z ) = .0. ) $. + $( If ` Z ` is the root of an irreducible polynomial ` P ` over a field + ` K ` , then the degree of the field extension ` [ K [ Z ] : K ] ` is + the degree of the polynomial ` P ` . $) + fldextdgirred $p |- ( ph -> ( L [:] K ) = ( D ` P ) ) $= ? $. + $} + + +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Quadratic field extensions +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + $c /FldExt2 $. + + $( Extend class notation with the quadratic field extension relation. $) + cfldext2 $a class /FldExt2 $. + + ${ + $d e f $. + $( Define the quadratic field extension relation. Quadratic field + extensions are field extensions of degree 2. $) + df-fldext2 $a |- /FldExt2 = { <. e , f >. | ( e /FldExt f /\ ( e [:] f ) = 2 ) } $. + $} + + +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Chain +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + $c Chain $. + + $( Extend class notation with the (finite) chain builder function. $) + cchn $a class Chain $. + + ${ + $d r c n $. + $( Define the (finite) chain builder function. A chain is defined to be a + sequence of objects, whereas each object is in a given relation with the + next one. $) + df-chn $a |- Chain = ( r e. _V |-> { c e. Word dom r | + A. n e. ( dom c \ { 0 } ) ( c ` ( n - 1 ) ) r ( c ` n ) } ) $. + $} + + +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Constructible points +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + $c Constr $. + + $( Extend class notation with the set of geometrically constructible points. $) + cconstr $a class Constr $. + + $( Define the set of geometrically constructible points, by recursively adding + the line-line, line-circle and circle-circle intersections constructions + using points in a previous iteration. $) + df-constr $a |- Constr = ( rec ( ( s e. _V |-> { x e. CC | + ( ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ -. ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) = 0 ) + \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) + \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s E. t e. RR ( -. a = d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) + } ) , { 0 , 1 } ) " _om ) $. + + ${ + constrtow2.b $e |- B = ( Base ` F ) $. + constrtow2.q $e |- Q = ( CCfld |`s QQ ) $. + constrtow2.a $e |- ( ph -> A e. Constr ) $. + constrtow2.f $e |- ( ph -> F e. Field ) $. + constrtow2.1 $e |- ( ph -> A e. B ) $. + $( If an algebraically constructible point ` A ` is in a field ` F ` , then + there is a tower of quadratic field extensions from ` QQ ` to ` F ` . $) + constrtow2 $p |- ( ph -> E. t e. ( Chain ` `' /FldExt2 ) ( ( t ` 0 ) = Q + /\ ( lastS ` t ) = F ) ) $= ? $. + $} + + +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Impossible constuctions +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + $( Impossibility of doubling the cube. This is expressed by stating that the + cubic root of 2, which is the side length of a cube of volume ` 2 ` , is + not constructible. $) + imp2cube $p |- -. ( 2 ^c ( 1 / 3 ) ) e. Constr $= ? $. + + $( Impossibility of trisecting angles. This is expressed by stating that the + cosine of an angle of ` ( _pi / 9 ) ` which would be the third of the + constructible angle ` ( _pi / 3 ) ` , is not constructible. $) + imp3ang $p |- -. ( cos ` ( _pi / 9 ) ) e. Constr $= ? $. From 10cf3961d72a0f78587dd9030adccf71d30265c5 Mon Sep 17 00:00:00 2001 From: tirix <5831830+tirix@users.noreply.github.com> Date: Fri, 17 Jan 2025 07:40:23 +0100 Subject: [PATCH 02/12] Update constr.mm Co-authored-by: icecream17 --- constr.mm | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/constr.mm b/constr.mm index 99c2145416..11f694de99 100644 --- a/constr.mm +++ b/constr.mm @@ -2,7 +2,7 @@ $( #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# - Contructible numbers + Constructible numbers #*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*# This section defines the set of constructible points as complex numbers which can be drawn starting from two points (we take ` 0 ` and ` 1 ` ), and taking From 7ac6a8d65e2ba0e4d477dba1b4a7c979bbba323a Mon Sep 17 00:00:00 2001 From: tirix <5831830+tirix@users.noreply.github.com> Date: Fri, 17 Jan 2025 07:40:40 +0100 Subject: [PATCH 03/12] Update constr.mm Co-authored-by: icecream17 --- constr.mm | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/constr.mm b/constr.mm index 11f694de99..b1cbc4fcff 100644 --- a/constr.mm +++ b/constr.mm @@ -124,7 +124,7 @@ can be drawn starting from two points (we take ` 0 ` and ` 1 ` ), and taking $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- - Impossible constuctions + Impossible constructions -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- $) From 12f03dc74855aad0171d0bf39d4e002f378576ef Mon Sep 17 00:00:00 2001 From: tirix <5831830+tirix@users.noreply.github.com> Date: Fri, 17 Jan 2025 07:41:23 +0100 Subject: [PATCH 04/12] Update constr.mm Co-authored-by: icecream17 --- constr.mm | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/constr.mm b/constr.mm index b1cbc4fcff..eb9f9969de 100644 --- a/constr.mm +++ b/constr.mm @@ -136,4 +136,4 @@ can be drawn starting from two points (we take ` 0 ` and ` 1 ` ), and taking $( Impossibility of trisecting angles. This is expressed by stating that the cosine of an angle of ` ( _pi / 9 ) ` which would be the third of the constructible angle ` ( _pi / 3 ) ` , is not constructible. $) - imp3ang $p |- -. ( cos ` ( _pi / 9 ) ) e. Constr $= ? $. + imp3ang $p |- -. ( cos ` ( _pi / 9 ) ) e. Constr $= ? $. From 30a91c9738a02d710d7517ae40b6cd102b19b172 Mon Sep 17 00:00:00 2001 From: tirix <5831830+tirix@users.noreply.github.com> Date: Fri, 17 Jan 2025 07:45:15 +0100 Subject: [PATCH 05/12] Update constr.mm Co-authored-by: icecream17 --- constr.mm | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/constr.mm b/constr.mm index eb9f9969de..f482eb891c 100644 --- a/constr.mm +++ b/constr.mm @@ -104,8 +104,8 @@ can be drawn starting from two points (we take ` 0 ` and ` 1 ` ), and taking the line-line, line-circle and circle-circle intersections constructions using points in a previous iteration. $) df-constr $a |- Constr = ( rec ( ( s e. _V |-> { x e. CC | - ( ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ -. ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) = 0 ) - \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) ) + ( E. a e. s E. b e. s E. c e. s E. d e. s E. t e. RR E. r e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ x = ( c + ( r x. ( d - c ) ) ) /\ -. ( Im ` ( ( * ` ( b - a ) ) x. ( d - c ) ) ) = 0 ) + \/ E. a e. s E. b e. s E. c e. s E. e e. s E. f e. s E. t e. RR ( x = ( a + ( t x. ( b - a ) ) ) /\ ( abs ` ( x - c ) ) = ( abs ` ( e - f ) ) ) \/ E. a e. s E. b e. s E. c e. s E. d e. s E. e e. s E. f e. s E. t e. RR ( -. a = d /\ ( abs ` ( x - a ) ) = ( abs ` ( b - c ) ) /\ ( abs ` ( x - d ) ) = ( abs ` ( e - f ) ) ) ) } ) , { 0 , 1 } ) " _om ) $. From de56b25ac1527ac5f9321d526fe29e44d1cd56ee Mon Sep 17 00:00:00 2001 From: tirix <5831830+tirix@users.noreply.github.com> Date: Sat, 18 Jan 2025 20:11:36 +0100 Subject: [PATCH 06/12] Update constr.mm Co-authored-by: icecream17 --- constr.mm | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/constr.mm b/constr.mm index f482eb891c..84c16b2ba5 100644 --- a/constr.mm +++ b/constr.mm @@ -32,7 +32,7 @@ can be drawn starting from two points (we take ` 0 ` and ` 1 ` ), and taking fldextdgirred.b $e |- B = ( Base ` F ) $. fldextdgirred.0 $e |- .0. = ( 0g ` F ) $. fldextdgirred.d $e |- D = ( deg1 ` F ) $. - fldextdgirred.o $e |- O = ( eval1 ` F ) $. + fldextdgirred.o $e |- O = ( F evalSub1 E ) $. fldextdgirred.m $e |- M = ( Poly1 ` F ) $. fldextdgirred.k $e |- K = ( F |`s E ) $. fldextdgirred.l $e |- L = ( F |`s ( F fldGen ( E u. { Z } ) ) ) $. From fb17c8c5be5f3a6e534f0d3bd3965f7fc07bf008 Mon Sep 17 00:00:00 2001 From: tirix <5831830+tirix@users.noreply.github.com> Date: Sun, 19 Jan 2025 02:27:05 +0100 Subject: [PATCH 07/12] Fix domain of polynomial Co-authored-by: icecream17 --- constr.mm | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/constr.mm b/constr.mm index 84c16b2ba5..d2f3bb0243 100644 --- a/constr.mm +++ b/constr.mm @@ -38,7 +38,7 @@ can be drawn starting from two points (we take ` 0 ` and ` 1 ` ), and taking fldextdgirred.l $e |- L = ( F |`s ( F fldGen ( E u. { Z } ) ) ) $. fldextdgirred.f $e |- ( ph -> F e. Field ) $. fldextdgirred.e $e |- ( ph -> E e. ( SubDRing ` F ) ) $. - fldextdgirred.p $e |- ( ph -> P e. ( Base ` M ) ) $. + fldextdgirred.p $e |- ( ph -> P e. dom O ) $. fldextdgirred.1 $e |- ( ph -> P e. ( Irred ` M ) ) $. fldextdgirred.z $e |- ( ph -> Z e. ( B \ E ) ) $. fldextdgirred.2 $e |- ( ph -> ( ( O ` P ) ` Z ) = .0. ) $. From 3bb90739eb12d914098b17f295ac4aeee1c7ea91 Mon Sep 17 00:00:00 2001 From: Thierry Arnoux <5831830+tirix@users.noreply.github.com> Date: Sun, 19 Jan 2025 02:29:28 +0100 Subject: [PATCH 08/12] Indentation --- constr.mm | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/constr.mm b/constr.mm index 99c2145416..ca66898cb7 100644 --- a/constr.mm +++ b/constr.mm @@ -136,4 +136,4 @@ can be drawn starting from two points (we take ` 0 ` and ` 1 ` ), and taking $( Impossibility of trisecting angles. This is expressed by stating that the cosine of an angle of ` ( _pi / 9 ) ` which would be the third of the constructible angle ` ( _pi / 3 ) ` , is not constructible. $) - imp3ang $p |- -. ( cos ` ( _pi / 9 ) ) e. Constr $= ? $. + imp3ang $p |- -. ( cos ` ( _pi / 9 ) ) e. Constr $= ? $. From 78fccb94aa4e94bd741c8b0f7d5aa1db277ac37c Mon Sep 17 00:00:00 2001 From: Thierry Arnoux <5831830+tirix@users.noreply.github.com> Date: Sun, 26 Jan 2025 15:17:32 +0100 Subject: [PATCH 09/12] Minimal polynomials --- changes-set.txt | 9 + constr.mm | 5 + set.mm | 678 ++++++++++++++++++++++++++++++++++++++---------- 3 files changed, 560 insertions(+), 132 deletions(-) diff --git a/changes-set.txt b/changes-set.txt index 0bbce40ec4..45673a61da 100644 --- a/changes-set.txt +++ b/changes-set.txt @@ -87,6 +87,15 @@ make a github issue.) DONE: Date Old New Notes +26-Jan-25 an2anr [same] Moved from PM's mathbox to main set.mm +26-Jan-25 ismhmd [same] Moved from SN's mathbox to main set.mm +26-Jan-25 ringcld [same] Moved from SN's mathbox to main set.mm +26-Jan-25 ablcmnd [same] Moved from SN's mathbox to main set.mm +26-Jan-25 ringabld [same] Moved from SN's mathbox to main set.mm +26-Jan-25 ringcmnd [same] Moved from SN's mathbox to main set.mm +26-Jan-25 pwsexpg [same] Moved from SN's mathbox to main set.mm +26-Jan-25 drnginvrcld [same] Moved from SN's mathbox to main set.mm +26-Jan-25 pwspjmhmmgpd [same] Moved from SN's mathbox to main set.mm 15-Jan-25 eqfunressuc [same] Moved from SF's mathbox to main set.mm 15-Jan-25 eqfunresadj [same] Moved from SF's mathbox to main set.mm 15-Jan-25 sotr3 [same] Moved from SF's mathbox to main set.mm diff --git a/constr.mm b/constr.mm index d2f3bb0243..cdc52d6bad 100644 --- a/constr.mm +++ b/constr.mm @@ -21,6 +21,11 @@ can be drawn starting from two points (we take ` 0 ` and ` 1 ` ), and taking cube ( ~ imp2cube ), and of angle trisection ( ~ imp3ang ) $) + $( All algebraic numbers admit a minimal polynomial. $) + $( minplyeu $p |- ( ph -> E! p e. ( Monic1p ` E ) A. q e. ( Monic1p ` E ) ( -> p = q ) ) $) + + $( Use infval $) + $( minplyf $) $( -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- diff --git a/set.mm b/set.mm index 96a6ed3d39..fbb6970229 100644 --- a/set.mm +++ b/set.mm @@ -5769,6 +5769,12 @@ use disjunction (although this is not required since definitions are ( wa anbi2d biancomd ) ADBFCDABCDEGH $. $} + $( Double commutation in conjunction. (Contributed by Peter Mazsa, + 27-Jun-2019.) $) + an2anr $p |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> + ( ( ps /\ ph ) /\ ( th /\ ch ) ) ) $= + ( wa ancom anbi12i ) ABEBAECDEDCEABFCDFG $. + $( Theorem *4.38 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.) $) pm4.38 $p |- ( ( ( ph <-> ch ) /\ ( ps <-> th ) ) -> @@ -227334,6 +227340,27 @@ everywhere defined internal operation (see ~ mndcl ), whose operation is SJKXEIVOVTVGWEWIWRWTWAWBWCWD $. $} + ${ + $d ph x y $. $d B x y $. $d F x y $. $d S x y $. $d T x y $. + ismhmd.b $e |- B = ( Base ` S ) $. + ismhmd.c $e |- C = ( Base ` T ) $. + ismhmd.p $e |- .+ = ( +g ` S ) $. + ismhmd.q $e |- .+^ = ( +g ` T ) $. + ismhmd.0 $e |- .0. = ( 0g ` S ) $. + ismhmd.z $e |- Z = ( 0g ` T ) $. + ismhmd.s $e |- ( ph -> S e. Mnd ) $. + ismhmd.t $e |- ( ph -> T e. Mnd ) $. + ismhmd.f $e |- ( ph -> F : B --> C ) $. + ismhmd.a $e |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> + ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) $. + ismhmd.h $e |- ( ph -> ( F ` .0. ) = Z ) $. + $( Deduction version of ~ ismhm . (Contributed by SN, 27-Jul-2024.) $) + ismhmd $p |- ( ph -> F e. ( S MndHom T ) ) $= + ( cmnd wcel wf cv cfv wceq wral w3a cmhm ralrimivva 3jca ismhm syl21anbrc + co ) AHUDUEIUDUEDEJUFZBUGZCUGZFUQJUHUSJUHUTJUHGUQUIZCDUJBDUJZKJUHLUIZUKJH + IULUQUESTAURVBVCUAAVABCDDUBUMUCUNBCDEFGHIJLKMNOPQRUOUP $. + $} + ${ $d f s t x y B $. $d x y F $. $d x y S $. $d x y T $. $( Reverse closure of a monoid homomorphism. (Contributed by Mario @@ -243514,6 +243541,14 @@ an extension of the previous (inserting an element and its inverse at ablcmn $p |- ( G e. Abel -> G e. CMnd ) $= ( cabl wcel cgrp ccmn isabl simprbi ) ABCADCAECAFG $. + ${ + ablcmnd.1 $e |- ( ph -> G e. Abel ) $. + $( An Abelian group is a commutative monoid. (Contributed by SN, + 1-Jun-2024.) $) + ablcmnd $p |- ( ph -> G e. CMnd ) $= + ( cabl wcel ccmn ablcmn syl ) ABDEBFECBGH $. + $} + ${ $d g x y B $. $d g x y G $. $d g .+ $. iscmn.b $e |- B = ( Base ` G ) $. @@ -252005,6 +252040,18 @@ the additive structure must be abelian (see ~ ringcom ), care must be HFUCDEUEUHGUDUAUB $. $} + ${ + ringcld.b $e |- B = ( Base ` R ) $. + ringcld.t $e |- .x. = ( .r ` R ) $. + ringcld.r $e |- ( ph -> R e. Ring ) $. + ringcld.x $e |- ( ph -> X e. B ) $. + ringcld.y $e |- ( ph -> Y e. B ) $. + $( Closure of the multiplication operation of a ring. (Contributed by SN, + 29-Jul-2024.) $) + ringcld $p |- ( ph -> ( X .x. Y ) e. B ) $= + ( crg wcel co ringcl syl3anc ) ACLMEBMFBMEFDNBMIJKBCDEFGHOP $. + $} + ${ ringdi.b $e |- B = ( Base ` R ) $. ringdi.p $e |- .+ = ( +g ` R ) $. @@ -252187,6 +252234,17 @@ the additive structure must be abelian (see ~ ringcom ), care must be ringcmn $p |- ( R e. Ring -> R e. CMnd ) $= ( crg wcel cabl ccmn ringabl ablcmn syl ) ABCADCAECAFAGH $. + ${ + ringabld.1 $e |- ( ph -> R e. Ring ) $. + $( A ring is an Abelian group. (Contributed by SN, 1-Jun-2024.) $) + ringabld $p |- ( ph -> R e. Abel ) $= + ( crg wcel cabl ringabl syl ) ABDEBFECBGH $. + + $( A ring is a commutative monoid. (Contributed by SN, 1-Jun-2024.) $) + ringcmnd $p |- ( ph -> R e. CMnd ) $= + ( ringabld ablcmnd ) ABABCDE $. + $} + ${ $d u v w x y B $. $d u v w x y K $. $d u v w x y ph $. $d u v w x y L $. ringpropd.1 $e |- ( ph -> B = ( Base ` K ) ) $. @@ -252920,6 +252978,65 @@ the additive structure must be abelian (see ~ ringcom ), care must be FWQWTXBWBWFHWLULXDVCWFLWOULXNVCVTSTWAWC $. $} + ${ + $d A a b x $. $d B a b x $. $d M a b $. $d R x $. $d T a b $. + $d Y x $. $d ph a b x $. + pwspjmhmmgpd.y $e |- Y = ( R ^s I ) $. + pwspjmhmmgpd.b $e |- B = ( Base ` Y ) $. + pwspjmhmmgpd.m $e |- M = ( mulGrp ` Y ) $. + pwspjmhmmgpd.t $e |- T = ( mulGrp ` R ) $. + pwspjmhmmgpd.r $e |- ( ph -> R e. Ring ) $. + pwspjmhmmgpd.i $e |- ( ph -> I e. V ) $. + pwspjmhmmgpd.a $e |- ( ph -> A e. I ) $. + $( The projection given by ~ pwspjmhm is also a monoid homomorphism between + the respective multiplicative groups. (Contributed by SN, + 30-Jul-2024.) $) + pwspjmhmmgpd $p |- ( ph -> ( x e. B |-> ( x ` A ) ) e. ( M MndHom T ) ) $= + ( cfv wcel wceq va vb cbs cmulr cv cmpt cur mgpbas mgpplusg ringidval crg + eqid cmnd pwsring syl2anc ringmgp syl wa adantr pwselbas ffvelcdmd fmpttd + simpr co cof simprl simprr pwsmulrval fveq1d ffnd inidm eqidd ofval eqtrd + mpidan ringcl syl3an1 3expb fveq1 fvex fvmpt oveq12d 3eqtr4d csn ringidcl + cxp 3syl pws1 fvconst2 3eqtr2d ismhmd ) AUAUBDEUCRZJUDRZEUDRZHFBDCBUEZRZU + FZJUGRZEUGRZDJHMLUHWLEFNWLULZUHJWMHMWMULZUIEWNFNWNULZUIJWRHMWRULZUJEWSFNW + SULZUJAJUKSZHUMSAEUKSZGISZXEOPEGIJKUNUOZJHMUPUQAXFFUMSOEFNUPUQABDWPWLAWOD + SZURZGWLCWOXJWLEGDUKWOJIKWTLAXFXIOUSAXGXIPUSAXIVCUTACGSZXIQUSVAVBAUAUEZDS + ZUBUEZDSZURZURZCXLXNWMVDZRZCXLRZCXNRZWNVDZXRWQRZXLWQRZXNWQRZWNVDXQXSCXLXN + WNVEVDZRZYBXQCXRYFXQDEWMWNXLXNGUKIJKLAXFXPOUSZAXGXPPUSZAXMXOVFZAXMXOVGZXB + XAVHVIAXPXKYGYBTQXQGGXTYAWNGXLXNIICXQGWLXLXQWLEGDUKXLJIKWTLYHYIYJUTVJXQGW + LXNXQWLEGDUKXNJIKWTLYHYIYKUTVJYIYIGVKXQXKURZXTVLYLYAVLVMVOVNXQXRDSZYCXSTA + XMXOYMAXEXMXOYMXHDJWMXLXNLXAVPVQVRBXRWPXSDWQCWOXRVSWQULZCXRVTWAUQXQYDXTYE + YAWNXQXMYDXTTYJBXLWPXTDWQCWOXLVSYNCXLVTWAUQXQXOYEYATYKBXNWPYADWQCWOXNVSYN + CXNVTWAUQWBWCAWRWQRZCWRRZCGWSWDWFZRZWSAXEWRDSYOYPTXHDJWRLXCWEBWRWPYPDWQCW + OWRVSYNCWRVTWAWGACYQWRAXFXGYQWRTOPEWSGIJKXDWHUOVIAXKYRWSTQGWSCEUGVTWIUQWJ + WK $. + $} + + ${ + $d A x $. $d B x $. $d N x $. $d R x $. $d X x $. $d Y x $. + $d .xb x $. $d ph x $. + pwsexpg.y $e |- Y = ( R ^s I ) $. + pwsexpg.b $e |- B = ( Base ` Y ) $. + pwsexpg.m $e |- M = ( mulGrp ` Y ) $. + pwsexpg.t $e |- T = ( mulGrp ` R ) $. + pwsexpg.s $e |- .xb = ( .g ` M ) $. + pwsexpg.g $e |- .x. = ( .g ` T ) $. + pwsexpg.r $e |- ( ph -> R e. Ring ) $. + pwsexpg.i $e |- ( ph -> I e. V ) $. + pwsexpg.n $e |- ( ph -> N e. NN0 ) $. + pwsexpg.x $e |- ( ph -> X e. B ) $. + pwsexpg.a $e |- ( ph -> A e. I ) $. + $( Value of a group exponentiation in a structure power. Compare + ~ pwsmulg . (Contributed by SN, 30-Jul-2024.) $) + pwsexpg $p |- ( ph -> ( ( N .xb X ) ` A ) = ( N .x. ( X ` A ) ) ) $= + ( vx cfv cmpt cmhm wcel cn0 wceq pwspjmhmmgpd mgpbas mhmmulg syl3anc cmnd + co crg pwsring syl2anc ringmgp syl mulgnn0cl fveq1 eqid fvex fvmpt oveq2d + cv 3eqtr3d ) AJLEUQZUECBUEVIZUFZUGZUFZJLVNUFZGUQZBVKUFZJBLUFZGUQAVNIFUHUQ + UIJUJUIZLCUIZVOVQUKAUEBCDFHIKMNOPQTUAUDULUBUCCEGVNIFJLCMIPOUMZRSUNUOAVKCU + IZVOVRUKAIUPUIZVTWAWCAMURUIZWDADURUIHKUIWETUADHKMNUSUTMIPVAVBUBUCCEIJLWBR + VCUOUEVKVMVRCVNBVLVKVDVNVEZBVKVFVGVBAVPVSJGAWAVPVSUKUCUELVMVSCVNBVLLVDWFB + LVFVGVBVHVJ $. + $} + ${ $d p q u v .+ $. $d a b p q u v w x y z ph $. $d a b p q u v w x y z U $. $d p q u x .1. $. $d p q u v w B $. $d a b p q u x y z F $. $d p q R $. @@ -254983,6 +255100,14 @@ nonzero elements form a group under multiplication (from which it ex 3imtr3d 3impib simprd ) BIJZDAJZDEKZLDCMZAJZUJEKZUGUHUIUKULNZUGDBOMZJZ UJUNJZUHUINUMUGBPJZUOUPQBRUQUOUPBUNCDUNSZHUAUCUBABUNDEFURGTABUNUJEFURGTUD UEUF $. + + drnginvrcld.r $e |- ( ph -> R e. DivRing ) $. + drnginvrcld.x $e |- ( ph -> X e. B ) $. + drnginvrcld.1 $e |- ( ph -> X =/= .0. ) $. + $( Closure of the multiplicative inverse in a division ring. ( ~ reccld + analog). (Contributed by SN, 14-Aug-2024.) $) + drnginvrcld $p |- ( ph -> ( I ` X ) e. B ) $= + ( cdr wcel wne cfv drnginvrcl syl3anc ) ACMNEBNEFOEDPBNJKLBCDEFGHIQR $. $} ${ @@ -452531,9 +452656,15 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the htmldef "[:]" as "[:]"; althtmldef "[:]" as "[:]"; latexdef "[:]" as "[:]"; -htmldef "fldGen" as "fldGen"; - althtmldef "fldGen" as "fldGen"; - latexdef "fldGen" as "\mathrm{fldGen}"; +htmldef "fldGen" as " fldGen "; + althtmldef "fldGen" as " fldGen"; + latexdef "fldGen" as "\mathbin{\operatorname{fldGen}}"; +htmldef "AlgNb" as " AlgNb "; + althtmldef "AlgNb" as " AlgNb "; + latexdef "AlgNb" as "\mathbin{\operatorname{AlgNb}}"; +htmldef "minPoly" as " minPoly "; + althtmldef "minPoly" as " minPoly "; + latexdef "minPoly" as "\mathbin{\operatorname{minPoly}}"; htmldef "repr" as "repr"; althtmldef "repr" as "repr"; @@ -474241,6 +474372,13 @@ and the expression ( x e. A /\ x e. B ) ` . ( wo w3o df-3or sylbir olcs ) ABFZCDKCFABCGDABCHEIJ $. $} + $( Associative law for four conjunctions with a triple conjunction. + (Contributed by Thierry Arnoux, 21-Jan-2025.) $) + 13an22anass $p |- ( ( ph /\ ( ps /\ ch /\ th ) ) <-> ( ( ph /\ ps ) /\ ( ch + /\ th ) ) ) $= + ( wa w3a an2anr an4 bitri an43 3bitr2ri 3an4anass ancom ) ABECDEEZBCEDAEEZB + CDFZAEAPEOCBEADEEZACEDBEEZNBCDAGRCAEBDEEQACDBGCABDHIACDBJKBCDALPAMK $. + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= @@ -491040,7 +491178,7 @@ such that every prime ideal contains a prime element (this is a fply1.3 $e |- P = ( Base ` ( Poly1 ` R ) ) $. fply1.4 $e |- ( ph -> F : ( NN0 ^m 1o ) --> B ) $. fply1.5 $e |- ( ph -> F finSupp .0. ) $. - $( Conditions for a function to be an univariate polynomial. (Contributed + $( Conditions for a function to be a univariate polynomial. (Contributed by Thierry Arnoux, 19-Aug-2023.) $) fply1 $p |- ( ph -> F e. P ) $= ( vf c1o co cfv wcel cfn cn0 cmap eqid cmps cbs cfsupp wbr ccnv cima crab @@ -491072,6 +491210,282 @@ such that every prime ideal contains a prime element (this is a PZVEAVQWCWEKMBDECGHJIUQTURUTVFVEAFGBUDVAVB $. $} + ${ + evls1scafv.q $e |- Q = ( S evalSub1 R ) $. + evls1scafv.w $e |- W = ( Poly1 ` U ) $. + evls1scafv.u $e |- U = ( S |`s R ) $. + evls1scafv.b $e |- B = ( Base ` S ) $. + evls1scafv.a $e |- A = ( algSc ` W ) $. + evls1scafv.s $e |- ( ph -> S e. CRing ) $. + evls1scafv.r $e |- ( ph -> R e. ( SubRing ` S ) ) $. + evls1scafv.x $e |- ( ph -> X e. R ) $. + evls1scafv.1 $e |- ( ph -> C e. B ) $. + $( Value of the univariate polynomial evaluation for a scalars. + (Contributed by Thierry Arnoux, 21-Jan-2025.) $) + evls1scafv $p |- ( ph -> ( ( Q ` ( A ` X ) ) ` C ) = X ) $= + ( cfv csn cxp evls1sca fveq1d wcel wceq fvconst2g syl2anc eqtrd ) ADJBTET + ZTDCJUAUBZTZJADUJUKABCEFGHIJKLMNOPQRUCUDAJFUEDCUEULJUFRSCJDFUGUHUI $. + $} + + ${ + evls1expd.q $e |- Q = ( S evalSub1 R ) $. + evls1expd.k $e |- K = ( Base ` S ) $. + evls1expd.w $e |- W = ( Poly1 ` U ) $. + evls1expd.u $e |- U = ( S |`s R ) $. + evls1expd.b $e |- B = ( Base ` W ) $. + evls1expd.s $e |- ( ph -> S e. CRing ) $. + evls1expd.r $e |- ( ph -> R e. ( SubRing ` S ) ) $. + evls1expd.1 $e |- ./\ = ( .g ` ( mulGrp ` W ) ) $. + evls1expd.2 $e |- .^ = ( .g ` ( mulGrp ` S ) ) $. + evls1expd.n $e |- ( ph -> N e. NN0 ) $. + evls1expd.m $e |- ( ph -> M e. B ) $. + evls1expd.c $e |- ( ph -> C e. K ) $. + $( Univariate polynomial evaluation builder for an exponential. See also + ~ evl1expd . (Contributed by Thierry Arnoux, 24-Jan-2025.) $) + evls1expd $p |- ( ph + -> ( ( Q ` ( N ./\ M ) ) ` C ) = ( N .^ ( ( Q ` M ) ` C ) ) ) $= + ( co cfv cpws cmgp cmg eqid evls1pw fveq1d cbs cvv crngringd wcel a1i crh + fvexi wf ccrg csubrg evls1rhm syl2anc rhmf syl ffvelcdmd pwsexpg eqtrd ) + ACLJKUFDUGZUGCLJDUGZFIUHUFZUIUGZUJUGZUFZUGLCVLUGHUFACVKVPABDEFGKMUIUGZILM + JNQPVQUKORUASTUCUDULUMACVMUNUGZFVOFUIUGZHIVNLUOVLVMVMUKZVRUKZVNUKVSUKVOUK + UBAFSUPIUOUQAIFUNOUTURUCABVRJDADMVMUSUFUQZBVRDVAAFVBUQEFVCUGUQWBSTIDEFVMG + MNOVTQPVDVEBVRMVMDRWAVFVGUDVHUEVIVJ $. + $} + + ${ + evls1varpwval.q $e |- Q = ( S evalSub1 R ) $. + evls1varpwval.u $e |- U = ( S |`s R ) $. + evls1varpwval.w $e |- W = ( Poly1 ` U ) $. + evls1varpwval.x $e |- X = ( var1 ` U ) $. + evls1varpwval.b $e |- B = ( Base ` S ) $. + evls1varpwval.e $e |- ./\ = ( .g ` ( mulGrp ` W ) ) $. + evls1varpwval.f $e |- .^ = ( .g ` ( mulGrp ` S ) ) $. + evls1varpwval.s $e |- ( ph -> S e. CRing ) $. + evls1varpwval.r $e |- ( ph -> R e. ( SubRing ` S ) ) $. + evls1varpwval.n $e |- ( ph -> N e. NN0 ) $. + evls1varpwval.c $e |- ( ph -> C e. B ) $. + $( Univariate polynomial evaluation for subrings maps the exponentiation of + a variable to the exponentiation of the evaluated variable. See + ~ evl1varpwval . (Contributed by Thierry Arnoux, 24-Jan-2025.) $) + evls1varpwval $p |- ( ph -> ( ( Q ` ( N ./\ X ) ) ` C ) = ( N .^ C ) ) + $= + ( co cfv cbs eqid csubrg wcel crg subrgring vr1cl 3syl evls1expd cid cres + evls1var fveq1d wceq fvresi syl eqtrd oveq2d ) ACJLIUDDUEUEJCLDUEZUEZHUDJ + CHUDAKUFUEZCDEFGHBLIJKMQONVFUGZTUARSUBAEFUHUEUIGUJUILVFUIUAEFGNUKVFKGLPOV + GULUMUCUNAVECJHAVECUOBUPZUEZCACVDVHABDEFGLMPNQTUAUQURACBUIVICUSUCBCUTVAVB + VCVB $. + $} + + ${ + ressply1evl.q $e |- Q = ( S evalSub1 R ) $. + ressply1evl.k $e |- K = ( Base ` S ) $. + ressply1evl.w $e |- W = ( Poly1 ` U ) $. + ressply1evl.u $e |- U = ( S |`s R ) $. + ressply1evl.b $e |- B = ( Base ` W ) $. + + ${ + $d .x. k $. $d .x. x $. $d A i j k $. $d A x $. $d B k $. + $d K k x $. $d M k $. $d Q k x $. $d S k $. $d S x $. $d U i j k $. + $d U x $. $d W i j k $. $d W x $. $d i j k ph $. $d ph x $. + evls1fpws.s $e |- ( ph -> S e. CRing ) $. + evls1fpws.r $e |- ( ph -> R e. ( SubRing ` S ) ) $. + evls1fpws.y $e |- ( ph -> M e. B ) $. + evls1fpws.1 $e |- .x. = ( .r ` S ) $. + evls1fpws.2 $e |- .^ = ( .g ` ( mulGrp ` S ) ) $. + evls1fpws.a $e |- A = ( coe1 ` M ) $. + $( Evaluation of a univariate subring polynomial as a function in a power + series. (Contributed by Thierry Arnoux, 23-Jan-2025.) $) + evls1fpws $p |- ( ph -> ( Q ` M ) = ( x e. K + |-> ( S gsum ( k e. NN0 |-> ( ( A ` k ) .x. ( k .^ x ) ) ) ) ) ) $= + ( vj vi cfv cn0 cv cv1 cmgp cmg co cvsca cmpt cgsu crg wcel wceq csubrg + subrgring syl eqid ply1coe syl2anc fveq2d cpws c0g wa csca cbs ply1lmod + clmod adantr coe1fvalcl sylan ply1sca eleqtrd cmnd ply1ring simpr vr1cl + ringmgp mgpbas mulgnn0cl syl3anc lmodvscl ssidd cvv fvexd fveq2 oveq12d + oveq1 clt wbr wral wrex coe1ae0 ad3antrrr eqtrd oveq1d ad4ant13 lmod0vs + wi ex imim2d ralimdva reximdva mpd mptnn0fsuppd evls1gsumadd cascl ccrg + cmulr crh evls1rhm wf ffvelcdmd rhmmul casa subrgcrng ply1assa asclmul1 + asclf cof fvexi a1i rhmf pwsmulrval pwselbas ffnd inidm ad2antrr simplr + wss mpteq2dva nn0ex csupp cfsupp ressbas2 eleqtrrd evls1varpwval offval + subrgss evls1scafv 3eqtr3d oveq2d crngringd sseldd ringcld 3impa 3com23 + ringcmnd 3expb wfun cfn mptexd coe1sfi fsuppimpd cdif csn cxp wfn coe1f + funmpt fvdifsupp subrg0 eqtr4d eldifad ringlz fconstmpt eqtr4di cmnmndd + pws0g suppss2 suppssfifsupp syl32anc pwsgsum 3eqtrd ) AMEUHNJUIJUJZCUHZ + UWAIUKUHZNULUHZUMUHZUNZNUOUHZUNZUPUQUNZEUHZBLGJUIUWBUWABUJZKUNZHUNZUPUQ + UNUPZAMUWIEAIURUSZMDUSZMUWIUTAFGVAUHUSZUWOUAFGIRVBVCZUBCDNIUWGJUWEMUWDU + WCQUWCVDZSUWGVDZUWDVDZUWEVDZUEVEVFVGAUWJGLVHUNZJUIUWHEUHZUPZUQUNUXCJUIB + LUWMUPZUPZUQUNUWNAJDUXCEFGILUINUWHNVIUHZOPQUXHVDZRUXCVDZSTUAAUWAUIUSZVJ + ZNVNUSZUWBNVKUHZVLUHZUSZUWFDUSZUWHDUSAUXMUXKAUWOUXMUWRNIQVMVCZVOUXLUWBI + VLUHZUXOAUWPUXKUWBUXSUSUBCDNIMUXSUWAUESQUXSVDZVPVQZAUXSUXOUTUXKAIUXNVLA + UWOIUXNUTZUWRNIURQVRVCZVGVOVSZUXLUWDVTUSZUXKUWCDUSZUXQUXLNURUSZUYEAUYGU + XKAUWOUYGUWRNIQWAVCZVONUWDUXAWDZVCAUXKWBUXLUWOUYFAUWOUXKUWRVODNIUWCUWSQ + SWCZVCDUWEUWDUWAUWCDNUWDUXASWEZUXBWFWGZUWBUWGUXNUXODNUWFSUXNVDZUWTUXOVD + ZWHWGZAUIWIAUFDUWHUFUJZCUHZUYPUWCUWEUNZUWGUNZJWJUXHUGANVIWKUYOUWAUYPUTU + WBUYQUWFUYRUWGUWAUYPCWLUWAUYPUWCUWEWNWMAUGUJZUYPWOWPZUYQIVIUHZUTZXEZUFU + IWQZUGUIWRZVUAUYSUXHUTZXEZUFUIWQZUGUIWRAUWPVUFUBCDNIUFMVUBUGUESQVUBVDZW + SVCAVUEVUIUGUIAUYTUIUSZVJZVUDVUHUFUIVULUYPUIUSZVJZVUCVUGVUAVUNVUCVUGVUN + VUCVJZUYSUXNVIUHZUYRUWGUNZUXHVUOUYQVUPUYRUWGVUOUYQVUBVUPVUNVUCWBVUOIUXN + VIAUYBVUKVUMVUCUYCWTVGXAXBVUOUXMUYRDUSZVUQUXHUTAUXMVUKVUMVUCUXRWTAVUMVU + RVUKVUCAVUMVJUYEVUMUYFVURAUYEVUMAUYGUYEUYHUYIVCVOAVUMWBAUYFVUMAUWOUYFUW + RUYJVCVODUWEUWDUYPUWCUYKUXBWFWGXCUWGUXNVUPDNUYRUXHSUYMUWTVUPVDUXIXDVFXA + XFXGXHXIXJXKXLAUXEUXGUXCUQAJUIUXDUXFUXLUWBNXMUHZUHZUWFNXOUHZUNZEUHZVUTE + UHZUWFEUHZUXCXOUHZUNZUXDUXFUXLENUXCXPUNUSZVUTDUSUXQVVCVVGUTAVVHUXKAGXNU + SZUWQVVHTUALEFGUXCINOPUXJRQXQVFVOZUXLUXODUWBVUSAUXODVUSXRUXKAVUSDUXNUXO + NVUSVDZUYMUYHUXRUYNSYEVOUYDXSZUYLVUTUWFNUXCVVAVVFEDSVVAVDZVVFVDZXTWGUXL + VVBUWHEUXLNYAUSZUXPUXQVVBUWHUTAVVOUXKAIXNUSZVVOAVVIUWQVVPTUAFGIRYBVFNIQ + YCVCVOUYDUYLVUSUWBUWGVVAUXNUXODNUWFVVKUYMUYNSVVMUWTYDWGVGUXLVVGVVDVVEHY + FUNUXFUXLUXCVLUHZGVVFHVVDVVELXNWJUXCUXJVVQVDZAVVIUXKTVOZLWJUSZUXLLGVLPY + GZYHZUXLDVVQVUTEUXLVVHDVVQEXRVVJDVVQNUXCESVVRYIVCZVVLXSZUXLDVVQUWFEVWCU + YLXSZUCVVNYJUXLBLLUWBUWLHLVVDVVEWJWJUXLLLVVDUXLLGLVVQXNVVDUXCWJUXJPVVRV + VSVWBVWDYKYLUXLLLVVEUXLLGLVVQXNVVEUXCWJUXJPVVRVVSVWBVWEYKYLVWBVWBLYMUXL + UWKLUSZVJZVUSLUWKEFGINUWBOQRPVVKAVVIUXKVWFTYNZAUWQUXKVWFUAYNZUXLUWBFUSV + WFUXLUWBUXSFUYAAFUXSUTZUXKAFLYPZVWJAUWQVWKUAFLGPUUEZVCFLIGRPUUAVCVOUUBZ + VOUXLVWFWBZUUFVWGLUWKEFGIKUWEUWANUWCORQUWSPUXBUDVWHVWIAUXKVWFYOZVWNUUCU + UDXAUUGYQUUHABJLGUWMLUIWJWJUXCUXCVIUHZUXJPVWPVDVVTAVWAYHZUIWJUSZAYRYHZA + GAGTUUIZUUNZAVWFUXKUWMLUSZAUXKVWFVXBAUXKVWFVXBVWGLGHUWBUWLPUCAGURUSZUXK + VWFVWTYNUXLUWBLUSVWFUXLFLUWBUXLUWQVWKAUWQUXKUAVOVWLVCVWMUUJVOVWGGULUHZV + TUSZUXKVWFUWLLUSZAVXEUXKVWFAVXCVXEVWTGVXDVXDVDZWDZVCYNVWOVWNLKVXDUWAUWK + LGVXDVXGPWEUDWFZWGUUKUULUUMUUOAUXGWJUSUXGUUPZVWPWJUSCVUBYSUNZUUQUSUXGVW + PYSUNVXKYPUXGVWPYTWPAJUIUXFWJVWSUURVXJAJUIUXFUVFYHAUXCVIWKACVUBAUWPCVUB + YTWPUBCDNIMVUBUESQVUJUUSVCUUTAUIUXFJWJVXKVWPAUWAUIVXKUVAUSZVJZUXFLGVIUH + ZUVBUVCZVWPVXMUXFBLVXNUPVXOVXMBLUWMVXNVXMVWFVJZUWMVXNUWLHUNZVXNVXPUWBVX + NUWLHVXMUWBVXNUTVWFVXMUWBVUBVXNVXMUICWJWJUWAVUBACUIUVDVXLAUIUXSCAUWPUIU + XSCXRUBCDNIMUXSUESQUXTUVEVCYLVOVWRVXMYRYHVXMIVIWKAVXLWBUVGAVXNVUBUTZVXL + AUWQVXRUAFGIVXNRVXNVDZUVHVCVOUVIVOXBVXPVXCVXFVXQVXNUTAVXCVXLVWFVWTYNZVX + PVXEUXKVWFVXFVXPVXCVXEVXTVXHVCVXPUWAUIVXKAVXLVWFYOUVJVXMVWFWBVXIWGLGHUW + LVXNPUCVXSUVKVFXAYQBLVXNUVLUVMAVXOVWPUTZVXLAGVTUSVVTVYAAGVXAUVNVWQGLWJU + XCVXNUXJVXSUVOVFVOXAVWSUVPVXKUXGWJWJVWPUVQUVRUVSUVTXA $. + $} + + ${ + $d B k m x $. $d E k m $. $d E k x $. $d K f x $. $d K k $. + $d K y $. $d Q k m $. $d Q k x $. $d R f x $. $d S f g x $. + $d S k $. $d U f x $. $d U k $. $d W k $. $d W x $. $d k m ph $. + $d k ph x $. + ressply1evl.e $e |- E = ( eval1 ` S ) $. + ressply1evl.s $e |- ( ph -> S e. CRing ) $. + ressply1evl.r $e |- ( ph -> R e. ( SubRing ` S ) ) $. + $( Evaluation of a univariate subring polynomial is the same as the + evaluation in the bigger ring. (Contributed by Thierry Arnoux, + 23-Jan-2025.) $) + ressply1evl $p |- ( ph -> Q = ( E |` B ) ) $= + ( cfv wcel eqid vm vx vk cres wceq cv wral wa cn0 cco1 cmgp cmg co cmpt + cmulr cgsu cress cpl1 cbs evl1fval1 adantr csubrg crg crngringd subrgid + ccrg syl cps1 ressply1bas2 inss2 eqsstrdi ressid fveq2d sseqtrrd sselda + cin evls1fpws simpr eqtr4d ralrimiva wfn wss cpws crh evl1rhm rhmf 3syl + wb wf ffnd evls1rhm syl2anc fvreseq1 syl21anc mpbird eqcomd ) AGBUDZCAW + QCUEZUAUFZGRZWSCRZUEZUABUGZAXBUABAWSBSZUHZWTUBHEUCUIUCUFZWSUJRZRXFUBUFE + UKRULRZUMEUORZUMUNUPUMUNXAXEUBXGEHUQUMZURRZUSRZGHEXIXJUCXHHWSXKHGEOKUTK + XKTXJTXLTAEVFSZXDPVAZAHEVBRZSZXDAEVCSXPAEPVDHEKVEVGVAABXLWSABEURRZUSRZX + LABFVHRZUSRZXRVPXRABXTEXQDIFXRXSXQTZMLNQXSTXTTXRTZVIXTXRVJVKZAXKXQUSAXJ + EURAXMXJEUEPHEVFKVLVGVMVMVNVOXITZXHTZXGTZVQXEUBXGBCDEXIFUCXHHWSIJKLMNXN + ADXOSZXDQVAAXDVRYDYEYFVQVSVTAGXRWACBWABXRWBWRXCWHAXREHWCUMZUSRZGAXMGXQY + HWDUMSXRYIGWIPHXQEYHGOYAYHTZKWEXRYIXQYHGYBYITZWFWGWJABYICACIYHWDUMSZBYI + CWIAXMYGYLPQHCDEYHFIJKYJMLWKWLBYIIYHCNYKWFVGWJYCUAXRBGCWMWNWOWP $. + $} + + ${ + evls1muld.1 $e |- .X. = ( .r ` W ) $. + evls1muld.2 $e |- .x. = ( .r ` S ) $. + evls1muld.s $e |- ( ph -> S e. CRing ) $. + evls1muld.r $e |- ( ph -> R e. ( SubRing ` S ) ) $. + evls1muld.m $e |- ( ph -> M e. B ) $. + evls1muld.n $e |- ( ph -> N e. B ) $. + evls1muld.c $e |- ( ph -> C e. K ) $. + $( Univariate polynomial evaluation of a product of polynomials. + (Contributed by Thierry Arnoux, 24-Jan-2025.) $) + evls1muld $p |- ( ph -> ( ( Q ` ( M .X. N ) ) ` C ) + = ( ( ( Q ` M ) ` C ) .x. ( ( Q ` N ) ` C ) ) ) $= + ( co ce1 cfv cpl1 cmulr cress wcel wceq eqid ressply1mul syl12anc oveqi + id cvv cbs fvexi ressmulr 3eqtr4g fveq2d fveq1d cres ressply1evl csubrg + crg subrgring ply1ring 3syl ringcld fvresd eqtr2d cps1 cin ressply1bas2 + ax-mp inss2 eqsstrdi sseldd jca evl1muld simprd 3eqtr3d ) ACKLHUFZFUGUH + ZUHZUHCKLFUIUHZUJUHZUFZWHUHZUHZCWGDUHZUHCKDUHZUHZCLDUHZUHZGUFZACWIWMAWG + WLWHAKLMUJUHZUFZKLWJBUKUFZUJUHZUFZWGWLAAKBULLBULXBXEUMAURUCUDABXCFWJEMI + KLWJUNZQPRUBXCUNZUOUPHXAKLSUQWKXDKLBUSULWKXDUMBMUTRVABWJXCWKUSXGWKUNZVB + VSUQVCVDVEACWIWOAWOWGWHBVFZUHWIAWGDXIABDEFIWHJMNOPQRWHUNZUAUBVGZVEAWGBW + HABMHKLRSAEFVHUHULIVIULMVIULUBEFIQVJMIPVKVLUCUDVMVNVOVEAWLWJUTUHZULWNWT + UMAJWJFWKGXLKLWHWQWSCXJXFOXLUNZUAUEAKXLULCKWHUHZUHWQUMABXLKABIVPUHZUTUH + ZXLVQXLABXPFWJEMIXLXOXFQPRUBXOUNXPUNXMVRXPXLVTWAZUCWBACXNWPAWPKXIUHXNAK + DXIXKVEAKBWHUCVNVOVEWCALXLULCLWHUHZUHWSUMABXLLXQUDWBACXRWRAWRLXIUHXRALD + XIXKVEALBWHUDVNVOVEWCXHTWDWEWF $. + $} + $} + + ${ + $d H f $. $d H h $. $d R f h $. $d h m $. + ressdeg1.h $e |- H = ( R |`s T ) $. + ressdeg1.d $e |- D = ( deg1 ` R ) $. + ressdeg1.u $e |- U = ( Poly1 ` H ) $. + ressdeg1.b $e |- B = ( Base ` U ) $. + ressdeg1.p $e |- ( ph -> P e. B ) $. + ressdeg1.t $e |- ( ph -> T e. ( SubRing ` R ) ) $. + $( The degree of a univariate polynomial in a structure restriction. + (Contributed by Thierry Arnoux, 20-Jan-2025.) $) + ressdeg1 $p |- ( ph -> ( D ` P ) = ( ( deg1 ` H ) ` P ) ) $= + ( cfv csupp cxr clt wcel eqid cco1 co csup cdg1 csubrg wceq subrg0 oveq2d + c0g syl supeq1d cpl1 cbs cps1 ressply1bas2 eleqtrd elin2d deg1val 3eqtr4d + cin ) ADUAOZEUIOZPUBZQRUCZVAHUIOZPUBZQRUCZDCOZDHUDOZOZAQVCVFRAVBVEVAPAFEU + EOSVBVEUFNFEHVBIVBTZUGUJUHUKADEULOZUMOZSVHVDUFAHUNOZUMOZVMDADBVOVMUTMABVO + EVLFGHVMVNVLTZIKLNVNTVOTVMTZUOUPUQVAVMCVLEDVBJVPVQVKVATZURUJADBSVJVGUFMVA + BVIGHDVEVITKLVETVRURUJUS $. + $} + + ${ + ply1ascl0.w $e |- W = ( Poly1 ` R ) $. + ply1ascl0.a $e |- A = ( algSc ` W ) $. + ply1ascl0.o $e |- O = ( 0g ` R ) $. + ply1ascl0.1 $e |- .0. = ( 0g ` W ) $. + ply1ascl0.r $e |- ( ph -> R e. Ring ) $. + $( The zero scalar as a polynomial. (Contributed by Thierry Arnoux, + 20-Jan-2025.) $) + ply1ascl0 $p |- ( ph -> ( A ` O ) = .0. ) $= + ( cascl cfv c0g csca crg wcel syl fveq2d eqid wceq ply1sca clmod ply1lmod + eqtrid ply1ring ascl0 eqtrd fveq1i 3eqtr4g ) ADELMZMZENMZDBMFAULEOMZNMZUK + MUMADUOUKADCNMUOIACUNNACPQZCUNUAKECPGUBRSUESAUKUNEUKTUNTAUPEUCQKECGUDRAUP + EPQKECGUFRUGUHDBUKHUIJUJ $. + $} + + ${ + ressply.1 $e |- S = ( Poly1 ` R ) $. + ressply.2 $e |- H = ( R |`s T ) $. + ressply.3 $e |- U = ( Poly1 ` H ) $. + ressply.4 $e |- B = ( Base ` U ) $. + ressply.5 $e |- ( ph -> T e. ( SubRing ` R ) ) $. + ${ + ressply10g.6 $e |- Z = ( 0g ` S ) $. + $( A restricted polynomial algebra has the same group identity (zero + polynomial). (Contributed by Thierry Arnoux, 20-Jan-2025.) $) + ressply10g $p |- ( ph -> Z = ( 0g ` U ) ) $= + ( c0g cfv cascl eqid wcel syl subrg1ascl fveq1d crg subrgring ply1ascl0 + cres csubrg wceq subrg0 csubg subrgsubg subg0cl eqeltrrd fvresd 3eqtr3d + 3syl fveq2d subrgrcl 3eqtr2rd ) AFOPZGOPZDQPZPZCOPZVBPHAVAFQPZPVAVBEUFZ + PUTVCAVAVEVFAVBVEDCEFGIVBRZJKMVERZUAUBAVEGVAFUTKVHVARUTRAECUGPSZGUCSMEC + GJUDTUEAVAEVBAVDVAEAVIVDVAUHMECGVDJVDRZUITZAVIECUJPSVDESMECUKECVDVJULUP + UMUNUOAVDVAVBVKUQAVBCVDDHIVGVJNAVICUCSMECURTUEUS $. + $} + + ${ + $d B p $. $d M p $. $d N p $. $d p ph $. + ressply1mon1p.m $e |- M = ( Monic1p ` R ) $. + ressply1mon1p.n $e |- N = ( Monic1p ` H ) $. + $( The monic polynomials of a restricted polynomial algebra. + (Contributed by Thierry Arnoux, 21-Jan-2025.) $) + ressply1mon1p $p |- ( ph -> N = ( B i^i M ) ) $= + ( wcel cfv wa eqid vp cin cv c0g wne cdg1 cco1 cur wceq w3a cbs ismon1p + anbi2i cress co ressply1bas ressbasss eqsstrdi sseld anbi1d 13an22anass + pm4.71d wb ressply10g neeq2d adantr simpr csubrg ressdeg1 fveq2d subrg1 + bitr4di syl eqeq12d anbi12d pm5.32da 3anass bitr3d bitr2id elin 3bitr4g + eqrdv ) AUAIBHUBZAUAUCZBQZWDFUDRZUEZWDGUFRZRZWDUGRZRZGUHRZUIZUJZWEWDHQZ + SZWDIQWDWCQWPWEWDDUKRZQZWDDUDRZUEZWDCUFRZRZWJRZCUHRZUIZUJZSZAWNWOXFWEWQ + XADCXDWDHWSJWQTZWSTZXATZOXDTZULUMAWEWTXESZSZXGWNAXMWEWRSZXLSXGAWEXNXLAW + EWRABWQWDABDBUNUOZUKRWQABXOCDEFGJKLMNXOTZUPBWQXODXPXHUQURUSVBUTWEWRWTXE + VAVLAXMWEWGWMSZSWNAWEXLXQAWESZWTWGXEWMAWTWGVCWEAWSWFWDABCDEFGWSJKLMNXIV + DVEVFXRXCWKXDWLXRXBWIWJXRBXAWDCEFGKXJLMAWEVGAECVHRQZWENVFVIVJAXDWLUIZWE + AXSXTNECGXDKXKVKVMVFVNVOVPWEWGWMVQVLVRVSBWHFGWLWDIWFLMWFTWHTPWLTULWDBHV + TWAWB $. + $} + $} + ${ $d P n $. $d R n $. ply1chr.1 $e |- P = ( Poly1 ` R ) $. @@ -492755,6 +493169,128 @@ such that every prime ideal contains a prime element (this is a $} +$( +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- + Algebraic numbers and Minimal polynomials +-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.- +$) + + $c AlgNb minPoly $. + + $( Extend class notation with the algebraic number builder function. $) + calgnb $a class AlgNb $. + + $( Extend class notation with the minimal polynomial builder function. $) + cminply $a class minPoly $. + + ${ + $( Define the minimal polynomial builder function. This definition is + similar to ~ df-aa . (Contributed by Thierry Arnoux, 19-Jan-2025.) $) + df-algnb $a |- AlgNb = ( e e. _V , f e. _V |-> U_ p e. ( dom ( e evalSub1 f + ) \ { ( 0g ` ( Poly1 ` e ) ) } ) ( `' ( ( e evalSub1 f ) ` p ) " { ( 0g + ` e ) } ) ) $. + $} + + ${ + $d e f p $. + $( Define the minimal polynomial builder function . (Contributed by + Thierry Arnoux, 19-Jan-2025.) $) + df-minply $a |- minPoly = ( e e. _V , f e. _V |-> ( x e. ( e AlgNb f ) |-> + inf ( ( `' ( ( e evalSub1 f ) ` p ) " { ( 0g ` e ) } ) , ( Monic1p ` e ) + , ( ( deg1 ` e ) oR < ( deg1 ` e ) ) ) ) ) $. + $} + + ${ + $d .0. e f $. $d E e f p $. $d F e f p $. $d O e f p $. $d Z e f p $. + algnbval.o $e |- O = ( E evalSub1 F ) $. + algnbval.z $e |- Z = ( 0g ` ( Poly1 ` E ) ) $. + algnbval.1 $e |- .0. = ( 0g ` E ) $. + algnbval.2 $e |- ( ph -> E e. Field ) $. + algnbval.3 $e |- ( ph -> F e. ( SubDRing ` E ) ) $. + $( The algebraic numbers over a field ` F ` within a field ` E ` . That + is, the numbers ` X ` which are roots of nonconstant polynomials + ` p ( X ) ` with coefficients in ` ( Base `` F ) ` . (Contributed by + Thierry Arnoux, 26-Jan-2025.) $) + algnbval $p |- ( ph -> ( E AlgNb F ) + = U_ p e. ( dom O \ { Z } ) ( `' ( O ` p ) " { .0. } ) ) $= + ( ve vf cvv wcel csn cfv ces1 c0g cdif cv ccnv cima ciun calgnb co cfield + cdm wceq elexd csdrg wral ovexi dmex difexi fvex cnvex imaex rgenw iunexg + a1i sylancl cpl1 wa oveq12 eqtr4di dmeqd simpl fveq2d sneqd fveq1d cnveqd + difeq12d imaeq12d iuneq12d df-algnb ovmpoga syl3anc ) ABOPCOPGDUIZFQZUAZG + UBZDRZUCZEQZUDZUEZOPZBCUFUGWHUJABUHKUKACBULRLUKAWBOPZWGOPZGWBUMWIWJAVTWAD + DBCSHUNUOUPVBWKGWBWEWFWDWCDUQURUSUTGWBWGOOVAVCMNBCOOGMUBZNUBZSUGZUIZWLVDR + ZTRZQZUAZWCWNRZUCZWLTRZQZUDZUEWHUFOWLBUJZWMCUJZVEZGWSWBXDWGXGWOVTWRWAXGWN + DXGWNBCSUGDWLBWMCSVFHVGZVHXGWQFXGWQBVDRZTRFXGWPXITXGWLBVDXEXFVIZVJVJIVGVK + VNXGXAWEXCWFXGWTWDXGWCWNDXHVLVMXGXBEXGXBBTREXGWLBTXJVJJVGVKVOVPMNGVQVRVS + $. + + ${ + $d B p $. $d E p $. $d F p $. $d O p $. $d X p $. $d Z p $. + $d p ph $. + isalgnb.b $e |- B = ( Base ` E ) $. + $( Property for an element ` X ` of a field ` E ` to be algebraic over a + subfield ` F ` . (Contributed by Thierry Arnoux, 26-Jan-2025.) $) + isalgnb $p |- ( ph -> ( X e. ( E AlgNb F ) <-> ( X e. B + /\ E. p e. ( dom O \ { Z } ) ( ( O ` p ) ` X ) = .0. ) ) ) $= + ( co wcel cfv wa eqid calgnb wceq cdm cdif wrex ccnv cima ciun algnbval + cv csn eleq2d eliun bitrdi wf wfn wb cpws cbs cfield adantr fvexi cress + cvv a1i cpl1 crh ccrg csubrg fldcrngd csdrg cdr issdrg simp2bi evls1rhm + syl syl2anc rhmf simpr eldifad fdmd eleqtrd ffvelcdmd pwselbas fniniseg + ffn 3syl rexbidva bitrd r19.42v ) AFCDUAPZQZFBQZFIUJZERZRGUBZSZIEUCZHUK + ZUDZUEZWMWPIWTUESAWLFWOUFGUKUGZQZIWTUEZXAAWLFIWTXBUHZQXDAWKXEFACDEGHIJK + LMNUIULIFWTXBUMUNAXCWQIWTAWNWTQZSZBBWOUOWOBUPXCWQUQXGBCBCBURPZUSRZUTWOX + HVDXHTZOXITZACUTQXFMVABVDQXGBCUSOVBVEXGCDVCPZVFRZUSRZXIWNEAXNXIEUOZXFAE + XMXHVGPQZXOACVHQDCVIRQZXPACMVJADCVKRQZXQNXRCVLQXQXLVLQCDVMVNVPBEDCXHXLX + MJOXJXLTXMTVOVQXNXIXMXHEXNTXKVRVPZVAXGWNWRXNXGWNWRWSAXFVSVTAWRXNUBXFAXN + XIEXSWAVAWBWCWDBBWOWFBGFWOWEWGWHWIWMWPIWTWJUN $. + $} + + ${ + $d .0. p q $. $d E p q $. $d F p q $. $d O p q $. $d X p q $. + $d Z p q $. $d p ph q $. + minplyeulem.x $e |- ( ph -> X e. ( E AlgNb F ) ) $. + $( An algebraic number ` X ` over ` F ` is a root of some monic + polynomial ` p ` with coefficients in ` F ` . (Contributed by Thierry + Arnoux, 26-Jan-2025.) $) + minplyeulem $p |- ( ph -> E. p e. ( Monic1p ` E ) ( ( O ` p ) ` X ) = .0. + ) $= + ( cfv wceq wcel eqid ad2antrr syl vq cv cmn1 wrex cdm csn cdif wa cress + co cdg1 cco1 cinvr cpl1 cascl cmulr cbs cin csdrg csubrg issdrg simp2bi + cdr ressply1mon1p inss2 eqsstrdi crg cuc1p simp3bi drngringd c0g simplr + wne eldifad cpws crh wf ccrg fldcrngd evls1rhm syl2anc eleqtrd eldifsni + rhmf fdmd ad2antlr ressply10g neeqtrd drnguc1p syl3anc uc1pmon1p sseldd + simpr fveq2d fveq1d eqeq1d csca casa fldsdrgfld ply1assa assaring clmod + cfield crngringd asclf deg1nn0cl coe1fvalcl deg1ldg drnginvrcld ply1sca + ply1lmod cn0 ffvelcdmd calgnb isalgnb mpbid simpld evls1muld oveq2d cvv + fvexd pwselbas ringrz 3eqtrd rspcedvd simprd r19.29a ) AEUAUBZDOOZFPZEH + UBZDOZOZFPZHBUCOZUDUADUEZGUFZUGZAYHYRQZUHZYJUHZYNEYHBCUIUJZUKOZOZYHULOZ + OZUUBUMOZOZUUBUNOZUOOZOZYHUUIUPOZUJZDOZOZFPHUUMYOUUAUUBUCOZYOUUMUUAUUPU + UIUQOZYOURYOUUAUUQBBUNOZCUUIUUBYOUUPUURRZUUBRZUUIRZUUQRZUUACBUSOQZCBUTO + QZAUVCYSYJMSUVCBVCQZUVDUUBVCQZBCVAZVBZTZYORUUPRZVDUUQYOVEVFUUAUUBVGQZYH + UUBVHOZQZUUMUUPQUUAUUBAUVFYSYJAUVCUVFMUVCUVEUVDUVFUVGVITSZVJZUUAUVFYHUU + QQZYHUUIVKOZVMZUVMUVNUUAYHYPUUQUUAYHYPYQAYSYJVLVNAYPUUQPYSYJAUUQBBUQOZV + OUJZUQOZDADUUIUVTVPUJQZUUQUWADVQZABVRQZUVDUWBABLVSZAUVCUVDMUVHTZUVSDCBU + VTUUBUUIIUVSRZUVTRZUUTUVAVTWAZUUQUWAUUIUVTDUVBUWARZWDZTWESWBZUUAYHGUVQY + SYHGVMAYJYHYPGWCWFAGUVQPYSYJAUUQBUURCUUIUUBGUUSUUTUVAUVBUWFJWGSWHZUUQUV + LUUIUUBYHUVQUVAUVBUVQRZUVLRZWIWJUUJUVLUUCUUIUUBUULUUGUUPYHUWOUVJUVAUULR + ZUUJRZUUCRZUUGRZWKWAWLUUAYKUUMPZUHZYMUUOFUXAEYLUUNUXAYKUUMDUUAUWTWMWNWO + WPUUAUUOEUUKDOZOZYIBUPOZUJUXCFUXDUJZFUUAUUQEDCBUXDUULUUBUVSUUKYHUUIIUWG + UVAUUTUVBUWPUXDRZAUWDYSYJUWESUVIUUAUUIWQOZUQOZUUQUUHUUJUUAUUJUUQUXGUXHU + UIUWQUXGRUUAUUIWRQZUUIVGQAUXIYSYJAUUBVRQUXIAUUBABXCQZUVCUUBXCQZLMCBWSWA + ZVSZUUIUUBUVAWTTSUUIXATAUUIXBQZYSYJAUVKUXNAUUBUXMXDUUIUUBUVAXKTSUXHRUVB + XEUUAUUHUUBUQOZUXHUUAUXOUUBUUGUUFUUBVKOZUXORZUXPRZUWSUVNUUAUVPUUDXLQZUU + FUXOQUWLUUAUVKUVPUVRUXSUVOUWLUWMUUQUUCUUIUUBYHUVQUWRUVAUWNUVBXFWJUUEUUQ + UUIUUBYHUXOUUDUUERZUVBUVAUXQXGWAUUAUVKUVPUVRUUFUXPVMUVOUWLUWMUUEUUQUUCU + UIUUBYHUXPUVQUWRUVAUWNUVBUXRUXTXHWJXIAUXOUXHPYSYJAUUBUXGUQAUXKUUBUXGPUX + LUUIUUBXCUVAXJTWNSWBXMZUWLAEUVSQZYSYJAUYBYJUAYRUDZAEBCXNUJQUYBUYCUHNAUV + SBCDEFGUAIJKLMUWGXOXPZXQSZXRUUAYIFUXCUXDYTYJWMXSUUABVGQZUXCUVSQUXEFPAUY + FYSYJABUWEXDSUUAUVSUVSEUXBUUAUVSBUVSUWAXCUXBUVTXTUWHUWGUWJAUXJYSYJLSUUA + BUQYAUUAUUQUWAUUKDUUAUWBUWCAUWBYSYJUWISUWKTUYAXMYBUYEXMUVSBUXDUXCFUWGUX + FKYCWAYDYEAUYBUYCUYDYFYG $. + $} + $} + + $( =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Matrices @@ -581852,12 +582388,6 @@ A collection of theorems for commuting equalities (or ( cv cvv wcel el3v3 elvd ) ABCACFGHBDEIJ $. $} - $( Double commutation in conjunction. (Contributed by Peter Mazsa, - 27-Jun-2019.) $) - an2anr $p |- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> - ( ( ps /\ ph ) /\ ( th /\ ch ) ) ) $= - ( wa ancom anbi12i ) ABEBAECDEDCEABFCDFG $. - $( Multiple commutations in conjunction. (Contributed by Peter Mazsa, 7-Mar-2020.) $) anan $p |- ( ( ( ( ph /\ ps ) /\ ch ) /\ ( ( ph /\ th ) /\ ta ) ) <-> @@ -657291,47 +657821,6 @@ D Fn ( I ... ( M - 1 ) ) /\ YPIQUAUDUOVULUPUJUMVUOYSABEJHUVDUVJFYPORUBUEUOVUNUPUKUNVUOYSWRYN $. $} - ${ - $d ph x y $. $d B x y $. $d F x y $. $d S x y $. $d T x y $. - ismhmd.b $e |- B = ( Base ` S ) $. - ismhmd.c $e |- C = ( Base ` T ) $. - ismhmd.p $e |- .+ = ( +g ` S ) $. - ismhmd.q $e |- .+^ = ( +g ` T ) $. - ismhmd.0 $e |- .0. = ( 0g ` S ) $. - ismhmd.z $e |- Z = ( 0g ` T ) $. - ismhmd.s $e |- ( ph -> S e. Mnd ) $. - ismhmd.t $e |- ( ph -> T e. Mnd ) $. - ismhmd.f $e |- ( ph -> F : B --> C ) $. - ismhmd.a $e |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> - ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) ) $. - ismhmd.h $e |- ( ph -> ( F ` .0. ) = Z ) $. - $( Deduction version of ~ ismhm . (Contributed by SN, 27-Jul-2024.) $) - ismhmd $p |- ( ph -> F e. ( S MndHom T ) ) $= - ( cmnd wcel wf cv cfv wceq wral w3a cmhm ralrimivva 3jca ismhm syl21anbrc - co ) AHUDUEIUDUEDEJUFZBUGZCUGZFUQJUHUSJUHUTJUHGUQUIZCDUJBDUJZKJUHLUIZUKJH - IULUQUESTAURVBVCUAAVABCDDUBUMUCUNBCDEFGHIJLKMNOPQRUOUP $. - $} - - ${ - ablcmnd.1 $e |- ( ph -> G e. Abel ) $. - $( An Abelian group is a commutative monoid. (Contributed by SN, - 1-Jun-2024.) $) - ablcmnd $p |- ( ph -> G e. CMnd ) $= - ( cabl wcel ccmn ablcmn syl ) ABDEBFECBGH $. - $} - - ${ - ringcld.b $e |- B = ( Base ` R ) $. - ringcld.t $e |- .x. = ( .r ` R ) $. - ringcld.r $e |- ( ph -> R e. Ring ) $. - ringcld.x $e |- ( ph -> X e. B ) $. - ringcld.y $e |- ( ph -> Y e. B ) $. - $( Closure of the multiplication operation of a ring. (Contributed by SN, - 29-Jul-2024.) $) - ringcld $p |- ( ph -> ( X .x. Y ) e. B ) $= - ( crg wcel co ringcl syl3anc ) ACLMEBMFBMEFDNBMIJKBCDEFGHOP $. - $} - ${ ringassd.b $e |- B = ( Base ` R ) $. ringassd.t $e |- .x. = ( .r ` R ) $. @@ -657370,17 +657859,6 @@ D Fn ( I ... ( M - 1 ) ) /\ ( crg wcel co wceq ringridm syl2anc ) ACLMFBMFEDNFOJKBCDEFGHIPQ $. $} - ${ - ringabld.1 $e |- ( ph -> R e. Ring ) $. - $( A ring is an Abelian group. (Contributed by SN, 1-Jun-2024.) $) - ringabld $p |- ( ph -> R e. Abel ) $= - ( crg wcel cabl ringabl syl ) ABDEBFECBGH $. - - $( A ring is a commutative monoid. (Contributed by SN, 1-Jun-2024.) $) - ringcmnd $p |- ( ph -> R e. CMnd ) $= - ( ringabld ablcmnd ) ABABCDE $. - $} - ${ $d C a b x y $. $d F a b $. $d M a b $. $d ph a b x y $. rncrhmcl.c $e |- C = ( N |`s ran F ) $. @@ -657449,17 +657927,12 @@ D Fn ( I ... ( M - 1 ) ) /\ LABHBAGIJ $. ${ - drnginvrcld.b $e |- B = ( Base ` R ) $. - drnginvrcld.0 $e |- .0. = ( 0g ` R ) $. - drnginvrcld.i $e |- I = ( invr ` R ) $. - drnginvrcld.r $e |- ( ph -> R e. DivRing ) $. - drnginvrcld.x $e |- ( ph -> X e. B ) $. - drnginvrcld.1 $e |- ( ph -> X =/= .0. ) $. - $( Closure of the multiplicative inverse in a division ring. ( ~ reccld - analog). (Contributed by SN, 14-Aug-2024.) $) - drnginvrcld $p |- ( ph -> ( I ` X ) e. B ) $= - ( cdr wcel wne cfv drnginvrcl syl3anc ) ACMNEBNEFOEDPBNJKLBCDEFGHIQR $. - + drnginvrn0d.b $e |- B = ( Base ` R ) $. + drnginvrn0d.0 $e |- .0. = ( 0g ` R ) $. + drnginvrn0d.i $e |- I = ( invr ` R ) $. + drnginvrn0d.r $e |- ( ph -> R e. DivRing ) $. + drnginvrn0d.x $e |- ( ph -> X e. B ) $. + drnginvrn0d.1 $e |- ( ph -> X =/= .0. ) $. $( A multiplicative inverse in a division ring is nonzero. ( ~ recne0d analog). (Contributed by SN, 14-Aug-2024.) $) drnginvrn0d $p |- ( ph -> ( I ` X ) =/= .0. ) $= @@ -657686,65 +658159,6 @@ D Fn ( I ... ( M - 1 ) ) /\ JKLSTUA $. $} - ${ - $d A a b x $. $d B a b x $. $d M a b $. $d R x $. $d T a b $. - $d Y x $. $d ph a b x $. - pwspjmhmmgpd.y $e |- Y = ( R ^s I ) $. - pwspjmhmmgpd.b $e |- B = ( Base ` Y ) $. - pwspjmhmmgpd.m $e |- M = ( mulGrp ` Y ) $. - pwspjmhmmgpd.t $e |- T = ( mulGrp ` R ) $. - pwspjmhmmgpd.r $e |- ( ph -> R e. Ring ) $. - pwspjmhmmgpd.i $e |- ( ph -> I e. V ) $. - pwspjmhmmgpd.a $e |- ( ph -> A e. I ) $. - $( The projection given by ~ pwspjmhm is also a monoid homomorphism between - the respective multiplicative groups. (Contributed by SN, - 30-Jul-2024.) $) - pwspjmhmmgpd $p |- ( ph -> ( x e. B |-> ( x ` A ) ) e. ( M MndHom T ) ) $= - ( cfv wcel wceq va vb cbs cmulr cv cmpt cur mgpbas mgpplusg ringidval crg - eqid cmnd pwsring syl2anc ringmgp syl wa adantr pwselbas ffvelcdmd fmpttd - simpr co cof simprl simprr pwsmulrval fveq1d ffnd inidm eqidd ofval eqtrd - mpidan ringcl syl3an1 3expb fveq1 fvex fvmpt oveq12d 3eqtr4d csn ringidcl - cxp 3syl pws1 fvconst2 3eqtr2d ismhmd ) AUAUBDEUCRZJUDRZEUDRZHFBDCBUEZRZU - FZJUGRZEUGRZDJHMLUHWLEFNWLULZUHJWMHMWMULZUIEWNFNWNULZUIJWRHMWRULZUJEWSFNW - SULZUJAJUKSZHUMSAEUKSZGISZXEOPEGIJKUNUOZJHMUPUQAXFFUMSOEFNUPUQABDWPWLAWOD - SZURZGWLCWOXJWLEGDUKWOJIKWTLAXFXIOUSAXGXIPUSAXIVCUTACGSZXIQUSVAVBAUAUEZDS - ZUBUEZDSZURZURZCXLXNWMVDZRZCXLRZCXNRZWNVDZXRWQRZXLWQRZXNWQRZWNVDXQXSCXLXN - WNVEVDZRZYBXQCXRYFXQDEWMWNXLXNGUKIJKLAXFXPOUSZAXGXPPUSZAXMXOVFZAXMXOVGZXB - XAVHVIAXPXKYGYBTQXQGGXTYAWNGXLXNIICXQGWLXLXQWLEGDUKXLJIKWTLYHYIYJUTVJXQGW - LXNXQWLEGDUKXNJIKWTLYHYIYKUTVJYIYIGVKXQXKURZXTVLYLYAVLVMVOVNXQXRDSZYCXSTA - XMXOYMAXEXMXOYMXHDJWMXLXNLXAVPVQVRBXRWPXSDWQCWOXRVSWQULZCXRVTWAUQXQYDXTYE - YAWNXQXMYDXTTYJBXLWPXTDWQCWOXLVSYNCXLVTWAUQXQXOYEYATYKBXNWPYADWQCWOXNVSYN - CXNVTWAUQWBWCAWRWQRZCWRRZCGWSWDWFZRZWSAXEWRDSYOYPTXHDJWRLXCWEBWRWPYPDWQCW - OWRVSYNCWRVTWAWGACYQWRAXFXGYQWRTOPEWSGIJKXDWHUOVIAXKYRWSTQGWSCEUGVTWIUQWJ - WK $. - $} - - ${ - $d A x $. $d B x $. $d N x $. $d R x $. $d X x $. $d Y x $. - $d .xb x $. $d ph x $. - pwsexpg.y $e |- Y = ( R ^s I ) $. - pwsexpg.b $e |- B = ( Base ` Y ) $. - pwsexpg.m $e |- M = ( mulGrp ` Y ) $. - pwsexpg.t $e |- T = ( mulGrp ` R ) $. - pwsexpg.s $e |- .xb = ( .g ` M ) $. - pwsexpg.g $e |- .x. = ( .g ` T ) $. - pwsexpg.r $e |- ( ph -> R e. Ring ) $. - pwsexpg.i $e |- ( ph -> I e. V ) $. - pwsexpg.n $e |- ( ph -> N e. NN0 ) $. - pwsexpg.x $e |- ( ph -> X e. B ) $. - pwsexpg.a $e |- ( ph -> A e. I ) $. - $( Value of a group exponentiation in a structure power. Compare - ~ pwsmulg . (Contributed by SN, 30-Jul-2024.) $) - pwsexpg $p |- ( ph -> ( ( N .xb X ) ` A ) = ( N .x. ( X ` A ) ) ) $= - ( vx cfv cmpt cmhm wcel cn0 wceq pwspjmhmmgpd mgpbas mhmmulg syl3anc cmnd - co crg pwsring syl2anc ringmgp syl mulgnn0cl fveq1 eqid fvex fvmpt oveq2d - cv 3eqtr3d ) AJLEUQZUECBUEVIZUFZUGZUFZJLVNUFZGUQZBVKUFZJBLUFZGUQAVNIFUHUQ - UIJUJUIZLCUIZVOVQUKAUEBCDFHIKMNOPQTUAUDULUBUCCEGVNIFJLCMIPOUMZRSUNUOAVKCU - IZVOVRUKAIUPUIZVTWAWCAMURUIZWDADURUIHKUIWETUADHKMNUSUTMIPVAVBUBUCCEIJLWBR - VCUOUEVKVMVRCVNBVLVKVDVNVEZBVKVFVGVBAVPVSJGAWAVPVSUKUCUELVMVSCVNBVLLVDWFB - LVFVGVBVHVJ $. - $} - ${ $d B x $. $d I a x y $. $d J a x y $. $d M a x $. $d R a $. $d T a $. $d U a $. $d Y a y $. $d ph a x y $. From 4b8831cc7e865d6e09cdaadc2068a5b54bf8e3d8 Mon Sep 17 00:00:00 2001 From: Thierry Arnoux <5831830+tirix@users.noreply.github.com> Date: Sun, 26 Jan 2025 15:27:30 +0100 Subject: [PATCH 10/12] Fix definitional soundness check. --- set.mm | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/set.mm b/set.mm index 99340c458e..7d0182d009 100644 --- a/set.mm +++ b/set.mm @@ -496103,6 +496103,7 @@ such that every prime ideal contains a prime element (this is a cminply $a class minPoly $. ${ + $d e f p $. $( Define the minimal polynomial builder function. This definition is similar to ~ df-aa . (Contributed by Thierry Arnoux, 19-Jan-2025.) $) df-algnb $a |- AlgNb = ( e e. _V , f e. _V |-> U_ p e. ( dom ( e evalSub1 f @@ -496111,7 +496112,7 @@ such that every prime ideal contains a prime element (this is a $} ${ - $d e f p $. + $d e f p x $. $( Define the minimal polynomial builder function . (Contributed by Thierry Arnoux, 19-Jan-2025.) $) df-minply $a |- minPoly = ( e e. _V , f e. _V |-> ( x e. ( e AlgNb f ) |-> From 6f85644fb09a9ddd146fd721508adaff86b165e5 Mon Sep 17 00:00:00 2001 From: Thierry Arnoux <5831830+tirix@users.noreply.github.com> Date: Sun, 26 Jan 2025 18:42:36 +0100 Subject: [PATCH 11/12] As per @savask remark --- set.mm | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/set.mm b/set.mm index 7d0182d009..8030b609ce 100644 --- a/set.mm +++ b/set.mm @@ -496104,7 +496104,7 @@ such that every prime ideal contains a prime element (this is a ${ $d e f p $. - $( Define the minimal polynomial builder function. This definition is + $( Define the algebraic number builder function. This definition is similar to ~ df-aa . (Contributed by Thierry Arnoux, 19-Jan-2025.) $) df-algnb $a |- AlgNb = ( e e. _V , f e. _V |-> U_ p e. ( dom ( e evalSub1 f ) \ { ( 0g ` ( Poly1 ` e ) ) } ) ( `' ( ( e evalSub1 f ) ` p ) " { ( 0g From 82795f747770ab1b271609b7550905741048d5f0 Mon Sep 17 00:00:00 2001 From: Thierry Arnoux <5831830+tirix@users.noreply.github.com> Date: Sun, 26 Jan 2025 23:18:36 +0100 Subject: [PATCH 12/12] As per @avekens comments --- set.mm | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/set.mm b/set.mm index 8030b609ce..a2fc3ca438 100644 --- a/set.mm +++ b/set.mm @@ -455586,7 +455586,7 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the althtmldef "[:]" as "[:]"; latexdef "[:]" as "[:]"; htmldef "fldGen" as " fldGen "; - althtmldef "fldGen" as " fldGen"; + althtmldef "fldGen" as " fldGen "; latexdef "fldGen" as "\mathbin{\operatorname{fldGen}}"; htmldef "AlgNb" as " AlgNb "; althtmldef "AlgNb" as " AlgNb "; @@ -494139,8 +494139,8 @@ such that every prime ideal contains a prime element (this is a evls1scafv.r $e |- ( ph -> R e. ( SubRing ` S ) ) $. evls1scafv.x $e |- ( ph -> X e. R ) $. evls1scafv.1 $e |- ( ph -> C e. B ) $. - $( Value of the univariate polynomial evaluation for a scalars. - (Contributed by Thierry Arnoux, 21-Jan-2025.) $) + $( Value of the univariate polynomial evaluation for scalars. (Contributed + by Thierry Arnoux, 21-Jan-2025.) $) evls1scafv $p |- ( ph -> ( ( Q ` ( A ` X ) ) ` C ) = X ) $= ( cfv csn cxp evls1sca fveq1d wcel wceq fvconst2g syl2anc eqtrd ) ADJBTET ZTDCJUAUBZTZJADUJUKABCEFGHIJKLMNOPQRUCUDAJFUEDCUEULJUFRSCJDFUGUHUI $. @@ -496128,9 +496128,11 @@ such that every prime ideal contains a prime element (this is a algnbval.2 $e |- ( ph -> E e. Field ) $. algnbval.3 $e |- ( ph -> F e. ( SubDRing ` E ) ) $. $( The algebraic numbers over a field ` F ` within a field ` E ` . That - is, the numbers ` X ` which are roots of nonconstant polynomials - ` p ( X ) ` with coefficients in ` ( Base `` F ) ` . (Contributed by - Thierry Arnoux, 26-Jan-2025.) $) + is, the numbers ` X ` which are roots of nonzero polynomials ` p ( X ) ` + with coefficients in ` ( Base `` F ) ` . This is expressed by the idiom + ` ( ``' ( O `` p ) " { .0. } ) ` , which can be translated into + ` { x e. ( Base `` E ) | ( ( O `` p ) `` x ) = .0. } ` by ~ fniniseg2 . + (Contributed by Thierry Arnoux, 26-Jan-2025.) $) algnbval $p |- ( ph -> ( E AlgNb F ) = U_ p e. ( dom O \ { Z } ) ( `' ( O ` p ) " { .0. } ) ) $= ( ve vf cvv wcel csn cfv ces1 c0g cdif cv ccnv cima ciun calgnb co cfield