:: Quadratic Extensions :: by Christoph Schwarzweller and Agnieszka Rowin\'nska-Schwarzweller :: :: Received November 30, 2021 :: Copyright (c) 2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies ARYTM_3, VECTSP_1, ALGSTR_0, TARSKI, STRUCT_0, SUBSET_1, NAT_1, SUPINF_2, BINOP_2, MESFUNC1, C0SP1, FUNCT_4, CARD_3, POLYNOM1, POLYNOM2, POLYNOM3, FUNCSDOM, ALGSEQ_1, EC_PF_1, HURWITZ, FINSEQ_1, RLVECT_3, CARD_1, VECTSP_2, FUNCT_1, RELAT_1, RLVECT_5, FOMODEL1, XBOOLE_0, NUMBERS, POLYNOM5, GROUP_1, FUNCT_7, ZFMISC_1, AFINSQ_1, REALALG2, REALSET1, LATTICE5, FDIFF_1, ALGNUM_1, ARYTM_1, FIELD_4, FIELD_2, FIELD_3, O_RING_1, YELLOW_8, PYTHTRIP, RATFUNC1, NEWTON, XXREAL_0, REALALG1, GAUSSINT, COMPLFLD, RING_5, GLIB_000, SQUARE_1, QC_LANG1, CAT_1, XCMPLX_0, INT_1, INT_3, FIELD_5, RING_3, FUNCT_2, MSSUBFAM, RLVECT_2, RLSUB_1, MOD_4, FIELD_6, FIELD_7, FIELD_8, FIELD_9; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, BINOP_1, RELAT_1, RELSET_1, REALSET1, FUNCT_1, ORDINAL1, FUNCT_2, MEMBERED, FUNCOP_1, NUMBERS, CARD_1, FINSEQ_1, ENUMSET1, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, NAT_D, SQUARE_1, INT_1, FUNCT_7, STRUCT_0, POLYNOM4, ALGSEQ_1, POLYNOM3, POLYNOM1, POLYNOM5, GROUP_1, GROUP_4, GROUP_6, MOD_4, VECTSP_4, VECTSP_6, VECTSP_7, VECTSP_9, BINOM, O_RING_1, GCD_1, ALGSTR_0, ALGSTR_1, QUOFIELD, INT_3, GR_CY_1, RLVECT_1, VECTSP_2, MATRLIN, HURWITZ, VECTSP_1, C0SP1, EC_PF_1, RATFUNC1, RINGCAT1, REALALG1, GAUSSINT, COMPLFLD, RING_2, RING_3, RING_4, RING_5, ALGNUM_1, FIELD_1, FIELD_2, FIELD_3, FIELD_4, FIELD_5, FIELD_6, FIELD_7, FIELD_8; constructors BINOP_1, REAL_1, FINSOP_1, BINARITH, VECTSP_2, POLYNOM3, C0SP1, ALGSTR_1, BHSP_1, MCART_1, NUMBERS, ZFMISC_1, RELAT_1, XREAL_0, FUNCOP_1, HURWITZ, VALUED_0, VECTSP_1, STRUCT_0, FUNCT_4, ARYTM_1, ARYTM_0, XCMPLX_0, XXREAL_0, SUBSET_1, FINSEQ_4, ORDINAL1, NAT_1, ALGSTR_0, NORMSP_1, FUNCT_2, FUNCT_1, POLYNOM4, XBOOLE_0, RELSET_1, ARYTM_3, ABIAN, QUOFIELD, PARTFUN1, RLVECT_1, FUNCT_7, NAT_D, FINSEQ_1, VFUNCT_1, CARD_1, FINSET_1, GAUSSINT, RATFUNC1, GCD_1, GROUP_6, FUNCT_5, REALSET1, O_RING_1, ALGSTR_2, INT_3, BINOM, RINGCAT1, MEMBERED, RING_2, RING_3, EC_PF_1, ALGSEQ_1, VECTSP_9, POLYNOM1, RING_4, GROUP_4, ALGNUM_1, ENUMSET1, GROUP_1, BINOP_2, GR_CY_1, RING_5, SQUARE_1, REALALG2, COMPLFLD, INT_1, POLYNOM5, FIELD_1, FIELD_2, FIELD_3, FIELD_4, FIELD_5, FIELD_6, FIELD_7, FIELD_8; registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, SUBSET_1, STRUCT_0, VECTSP_1, ALGSTR_1, EC_PF_1, FINSET_1, FUNCT_2, ALGSTR_0, GROUP_1, RLVECT_1, QUOFIELD, FUNCT_1, PARTFUN1, VFUNCT_1, CARD_1, REALSET1, RATFUNC1, GAUSSINT, MOD_4, COMPLFLD, RELAT_1, RINGCAT1, FINSEQ_1, POLYNOM1, POLYNOM3, POLYNOM5, RING_2, RING_3, RING_4, RING_5, REALALG1, REALALG2, FIELD_2, FIELD_4, FIELD_5, FIELD_6, FIELD_7; requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM; begin :: Preliminaries theorem :: FIELD_9:1 for a,b being Nat st a <= b holds a -' 1 <= b -' 1; registration let i be Integer; cluster i^2 -> integer; end; definition let R be Ring, S be RingExtension of R; let a be R-membered Element of S; func @a -> Element of R equals :: FIELD_9:def 1 a; end; registration let R be Ring, S be RingExtension of R; let a be R-membered Element of S; cluster -a -> R-membered; end; registration let R be Ring, S be RingExtension of R; let a,b be R-membered Element of S; cluster a + b -> R-membered; cluster a * b -> R-membered; end; registration let R be Ring, S be RingExtension of R; cluster 0.S -> R-membered; end; registration let R be non degenerated Ring, S be RingExtension of R; cluster 1.S -> non zero R-membered; end; registration let R be non degenerated Ring, S be RingExtension of R; cluster non zero R-membered for Element of S; end; registration let F be Field, E be FieldExtension of F; let a be non zero F-membered Element of E; cluster a" -> F-membered; end; registration let R be Ring; let a,b,c be Element of R; cluster <*a,b,c*> -> (the carrier of R)-valued; end; registration cluster non 2-characteristic strict for Field; end; registration let R be Ring; reduce (0.R)^2 to 0.R; reduce (1.R)^2 to 1.R; reduce (-(1.R))^2 to 1.R; end; theorem :: FIELD_9:2 for R being comRing, a,b being Element of R holds (a * b)^2 = a^2 * b^2; theorem :: FIELD_9:3 for F being Field, a being Element of F, b being non zero Element of F for i being Integer st i '*' a <> 0.F & i '*' b <> 0.F holds (i '*' a) * ((i '*' b)") = a * b"; theorem :: FIELD_9:4 for R being comRing for a being Element of R, i being Integer holds (i '*' a)^2 = i^2 '*' a^2; theorem :: FIELD_9:5 for R being non 2-characteristic domRing for a being Element of R holds 2 '*' a = 0.R iff a = 0.R; theorem :: FIELD_9:6 for R being non 2-characteristic domRing for a being Element of R holds 4 '*' a = 0.R iff a = 0.R; theorem :: FIELD_9:7 for R being Ring, S being RingExtension of R for a being Element of R, b being Element of S st b = a for i being Integer holds i '*' a = i '*' b; theorem :: FIELD_9:8 for R being domRing, S being domRingExtension of R for a being Element of R, b being Element of S st b^2 = a^2 holds b = a or b = -a; theorem :: FIELD_9:9 for F being Field, E being FieldExtension of F for a being Element of E holds FAdj(F,{a,-a}) = FAdj(F,{a}); theorem :: FIELD_9:10 for F being Field, E being FieldExtension of F for a being Element of E holds FAdj(F,{a}) = FAdj(F,{-a}); registration cluster non algebraic-closed for polynomial_disjoint Field; end; registration let F be non algebraic-closed Field; cluster irreducible non linear for Element of the carrier of Polynom-Ring F; end; registration let F be Field; cluster irreducible non linear -> non with_roots for Element of the carrier of Polynom-Ring F; cluster irreducible with_roots -> linear for Element of the carrier of Polynom-Ring F; end; registration let F be polynomial_disjoint Field; let p be irreducible Element of the carrier of Polynom-Ring F; cluster KrRootP p -> F-algebraic; end; registration let F be non algebraic-closed polynomial_disjoint Field; let p be irreducible non linear Element of the carrier of Polynom-Ring F; cluster KrRootP p -> non zero non F-membered; end; begin theorem :: FIELD_9:11 for R being non degenerated Ring, p being non zero Polynomial of R for q being Polynomial of R holds deg(p*'q) <= deg p + deg q; registration let L be well-unital non degenerated doubleLoopStr; let k be non zero Element of NAT; let a be Element of L; cluster rpoly(k,a) -> monic; end; registration let R be non degenerated Ring; let a be non zero Element of R, b be Element of R; cluster <%b,a%> -> linear; end; registration let R be non degenerated Ring; let b be Element of R; cluster <%b,1.R%> -> monic linear; end; theorem :: FIELD_9:12 for R being Ring for a,b,x being Element of R holds x * <%b,a%> = <%x*b,x*a%>; theorem :: FIELD_9:13 for R being Ring, p being Polynomial of R st deg p < 2 for a being Element of R ex y,z being Element of R st p = <%y,z%>; theorem :: FIELD_9:14 for R being comRing, p being Polynomial of R st deg p < 2 for a being Element of R ex y,z being Element of R st eval(p,a) = y + a * z; theorem :: FIELD_9:15 for F being Field, E being FieldExtension of F for p being Polynomial of F st deg p < 2 for a being Element of E ex y,z being F-membered Element of E st Ext_eval(p,a) = y + a * z; definition let R be Ring; let a be Element of R; func X-a -> Element of the carrier of Polynom-Ring R equals :: FIELD_9:def 2 rpoly(1,a); func X+a -> Element of the carrier of Polynom-Ring R equals :: FIELD_9:def 3 rpoly(1,-a); end; registration let R be non degenerated Ring; let a be Element of R; cluster X-a -> linear monic; cluster X+a -> linear monic; end; begin :: Quadratic Polynomials definition let R be Ring; let p be Polynomial of R; attr p is quadratic means :: FIELD_9:def 4 deg p = 2; end; registration let R be non degenerated Ring; cluster monic quadratic for Polynomial of R; cluster monic quadratic for Element of the carrier of Polynom-Ring R; end; registration let R be non degenerated Ring; cluster -> non constant for quadratic Polynomial of R; cluster -> non constant for quadratic Element of the carrier of Polynom-Ring R; end; definition let L be non empty ZeroStr; let a,b,c be Element of L; func <%c,b,a%> -> sequence of L equals :: FIELD_9:def 5 0_.(L)+*(0,c)+*(1,b)+*(2,a); end; registration let L be non empty ZeroStr; let a,b,c be Element of L; cluster <%c,b,a%> -> finite-Support; end; theorem :: FIELD_9:16 for L being non empty ZeroStr for a,b,c being Element of L holds <%c,b,a%>.0 = c & <%c,b,a%>.1 = b & <%c,b,a%>.2 = a & for n being Nat st n >= 3 holds <%c,b,a%>.n = 0.L; theorem :: FIELD_9:17 for L being non empty ZeroStr for a,b,c being Element of L holds deg <%c,b,a%> <= 2; theorem :: FIELD_9:18 for L being non empty ZeroStr for a,b,c being Element of L holds deg <%c,b,a%> = 2 iff a <> 0.L; registration let R be non degenerated Ring; let a be non zero Element of R, b,c be Element of R; cluster <%c,b,a%> -> quadratic; end; registration let R be non degenerated Ring; let b,c be Element of R; cluster <%c,b,1.R%> -> quadratic monic; end; registration let R be domRing; let a,x be non zero Element of R, b,c be Element of R; cluster x * <%c,b,a%> -> quadratic; end; theorem :: FIELD_9:19 for R being Ring for a,b,c,x being Element of R holds x * <%c,b,a%> = <%x*c,x*b,x*a%>; theorem :: FIELD_9:20 for R being Ring for a,b,c,x being Element of R holds eval(<%c,b,a%>,x) = c + b * x + a * x^2; theorem :: FIELD_9:21 for R being non degenerated Ring, p being Polynomial of R holds p is quadratic iff ex a being non zero Element of R, b,c being Element of R st p = <%c,b,a%>; theorem :: FIELD_9:22 for R being non degenerated Ring, p being monic Polynomial of R holds p is quadratic iff ex b,c being Element of R st p = <%c,b,1.R%>; theorem :: FIELD_9:23 for R being non degenerated Ring, S being RingExtension of R for a1,b1,c1 being Element of R, a2,b2,c2 being Element of S st a1 = a2 & b1 = b2 & c1 = c2 holds <%c2,b2,a2%> = <%c1,b1,a1%>; definition let R be non degenerated Ring; let p be Polynomial of R; attr p is purely_quadratic means :: FIELD_9:def 6 ex a being non zero Element of R, c being Element of R st p = <%c,0.R,a%>; end; registration let R be non degenerated Ring; let a be non zero Element of R, c be Element of R; cluster <%c,0.R,a%> -> purely_quadratic; end; registration let R be non degenerated Ring; cluster monic purely_quadratic for Polynomial of R; end; registration let R be non degenerated Ring; cluster purely_quadratic -> quadratic for Polynomial of R; end; definition let R be Ring; let a be Element of R; func X^2-a -> Element of the carrier of Polynom-Ring R equals :: FIELD_9:def 7 <%-a,0.R,1.R%>; func X^2+a -> Element of the carrier of Polynom-Ring R equals :: FIELD_9:def 8 <%a,0.R,1.R%>; end; registration let R be non degenerated Ring; cluster linear -> non quadratic for Polynomial of R; cluster quadratic -> non linear for Polynomial of R; end; registration let R be non degenerated Ring; let a be Element of R; cluster X^2-a -> purely_quadratic monic non constant; cluster X^2+a -> purely_quadratic monic non constant; end; theorem :: FIELD_9:24 for F being Field for b1,c1,b2,c2 being Element of F holds <%c1,b1%> *' <%c2,b2%> = <%c1*c2,b1*c2+b2*c1,b1*b2%>; theorem :: FIELD_9:25 for F being non 2-characteristic Field for a being non zero Element of F, b,c being Element of F for w being Element of F st w^2 = b^2 - 4 '*' a * c holds eval(<%c,b,a%>,(-b + w) * (2 '*' a)") = 0.F & eval(<%c,b,a%>,(-b - w) * (2 '*' a)") = 0.F; theorem :: FIELD_9:26 for F being Field for a being non zero Element of F, b,c being Element of F st Roots <%c,b,a%> <> {} holds b^2 - 4 '*' a * c is square; theorem :: FIELD_9:27 for F being non 2-characteristic Field for a being non zero Element of F, b,c being Element of F for w being Element of F st w^2 = b^2 - 4 '*' a * c holds Roots <%c,b,a%> = { (-b + w) * (2 '*' a)", (-b - w) * (2 '*' a)" }; theorem :: FIELD_9:28 for F being non 2-characteristic Field for a being non zero Element of F, b,c being Element of F for w being Element of F st w^2 = b^2 - 4 '*' a * c for r1,r2 being Element of F st r1 = (-b + w) * (2 '*' a)" & r2 = (-b - w) * (2 '*' a)" holds <%c,b,a%> = a * (X-r1) *' (X-r2); definition let R be non degenerated Ring; let p be quadratic Polynomial of R; func Discriminant p -> Element of R means :: FIELD_9:def 9 ex a being non zero Element of R, b,c being Element of R st p = <%c,b,a%> & it = b^2 - 4 '*' a * c; end; notation let R be non degenerated Ring; let p be quadratic Polynomial of R; synonym DC p for Discriminant p; end; definition let R be non degenerated Ring; let p be monic quadratic Polynomial of R; redefine func Discriminant p means :: FIELD_9:def 10 ex b,c being Element of R st p = <%c,b,1.R%> & it = b^2 - 4 '*' c; end; definition let R be non degenerated Ring; let p be monic purely_quadratic Polynomial of R; redefine func Discriminant p means :: FIELD_9:def 11 ex c being Element of R st p = <%c,0.R,1.R%> & it = - 4 '*' c; end; theorem :: FIELD_9:29 for F being non 2-characteristic Field, p being quadratic Polynomial of F holds Roots p <> {} iff DC p is square; theorem :: FIELD_9:30 for F being non 2-characteristic Field, p being quadratic Polynomial of F holds card(Roots p) = 1 iff DC p = 0.F; theorem :: FIELD_9:31 for F being non 2-characteristic Field, p being quadratic Polynomial of F holds card(Roots p) = 2 iff DC p is non zero square; theorem :: FIELD_9:32 for F being non 2-characteristic Field for p being quadratic Element of the carrier of Polynom-Ring F holds p is reducible iff DC p is square; theorem :: FIELD_9:33 for F being non 2-characteristic Field for a being Element of F holds X^2-a is reducible iff a is square; begin :: Quadratic Polynomials over Z/2 theorem :: FIELD_9:34 the carrier of Z/2 = { 0.(Z/2), 1.(Z/2) }; theorem :: FIELD_9:35 - 1.(Z/2) = 1.(Z/2); registration cluster Z/2 -> polynomial_disjoint; end; registration cluster -> square for Element of Z/2; end; registration cluster -> monic for non zero Polynomial of Z/2; cluster -> monic for non zero Element of the carrier of Polynom-Ring Z/2; end; definition func X^2 -> quadratic Element of the carrier of Polynom-Ring Z/2 equals :: FIELD_9:def 12 <%0.(Z/2),0.(Z/2),1.(Z/2)%>; func X^2+1 -> quadratic Element of the carrier of Polynom-Ring Z/2 equals :: FIELD_9:def 13 <%1.(Z/2),0.(Z/2),1.(Z/2)%>; func X^2+X -> quadratic Element of the carrier of Polynom-Ring Z/2 equals :: FIELD_9:def 14 <%0.(Z/2),1.(Z/2),1.(Z/2)%>; func X^2+X+1 -> quadratic Element of the carrier of Polynom-Ring Z/2 equals :: FIELD_9:def 15 <%1.(Z/2),1.(Z/2),1.(Z/2)%>; func X_ -> linear Element of the carrier of Polynom-Ring Z/2 equals :: FIELD_9:def 16 <%0.(Z/2),1.(Z/2)%>; func X-1 -> linear Element of the carrier of Polynom-Ring Z/2 equals :: FIELD_9:def 17 <%1.(Z/2),1.(Z/2)%>; end; theorem :: FIELD_9:36 the set of all p where p is quadratic Polynomial of Z/2 = { X^2, X^2+1, X^2+X, X^2+X+1 }; theorem :: FIELD_9:37 card(the set of all p where p is quadratic Polynomial of Z/2) = 4; theorem :: FIELD_9:38 for p being quadratic Polynomial of Z/2 holds DC p is square; theorem :: FIELD_9:39 X^2 = X_ *' X_ & Roots X^2 = { 0.(Z/2) }; theorem :: FIELD_9:40 X^2+1 = (X-1) *' (X-1) & Roots X^2+1 = { 1.(Z/2) }; theorem :: FIELD_9:41 X^2+X = X_ *' (X-1) & Roots X^2+X = { 0.(Z/2), 1.(Z/2) }; theorem :: FIELD_9:42 Roots X^2+X+1 = {}; registration cluster X^2 -> reducible; cluster X^2+1 -> reducible; cluster X^2+X -> reducible; cluster X^2+X+1 -> irreducible; end; theorem :: FIELD_9:43 Z/2 is SplittingField of X^2; theorem :: FIELD_9:44 Z/2 is SplittingField of X^2+1; theorem :: FIELD_9:45 Z/2 is SplittingField of X^2+X; definition func alpha -> Element of embField(canHomP X^2+X+1) equals :: FIELD_9:def 18 KrRootP X^2+X+1; end; definition func alpha-1 -> Element of embField(canHomP X^2+X+1) equals :: FIELD_9:def 19 alpha - 1.embField(canHomP X^2+X+1); end; registration cluster alpha -> non zero (Z/2)-algebraic; end; theorem :: FIELD_9:46 -alpha = alpha & alpha" = alpha-1 & alpha" <> alpha; theorem :: FIELD_9:47 X^2+X+1 = (X-alpha) *' (X-alpha") = (X-alpha) *' (X-(alpha-1)); theorem :: FIELD_9:48 Roots(FAdj(Z/2,{alpha}),X^2+X+1) = { alpha, alpha-1 }; theorem :: FIELD_9:49 card Roots(FAdj(Z/2,{alpha}),X^2+X+1) = 2; theorem :: FIELD_9:50 MinPoly(alpha,Z/2) = X^2+X+1; theorem :: FIELD_9:51 deg(FAdj(Z/2,{alpha}),Z/2) = 2; theorem :: FIELD_9:52 FAdj(Z/2,{alpha}) is SplittingField of X^2+X+1; begin :: Fields with non-squares definition let R be Ring; attr R is quadratic_complete means :: FIELD_9:def 20 the carrier of R c= SQ R; end; registration cluster -1.F_Real -> non square; cluster -1.F_Rat -> non square; end; registration cluster algebraic-closed -> quadratic_complete for non degenerated Ring; cluster preordered -> non quadratic_complete for non degenerated Ring; end; registration cluster F_Rat -> non quadratic_complete; cluster F_Real -> non quadratic_complete; cluster F_Complex -> quadratic_complete; end; registration cluster non quadratic_complete polynomial_disjoint strict for Field; cluster quadratic_complete strict for Field; end; registration cluster non quadratic_complete -> non degenerated for Ring; end; registration let R be non quadratic_complete Ring; cluster non square for Element of R; end; registration cluster strict polynomial_disjoint non quadratic_complete non 2-characteristic for Field; end; registration let F be non quadratic_complete non 2-characteristic Field; cluster monic quadratic irreducible for Element of the carrier of Polynom-Ring F; end; registration let F be non 2-characteristic Field; let a be square Element of F; cluster X^2-a -> reducible; end; registration let F be non quadratic_complete non 2-characteristic Field; let a be non square Element of F; cluster X^2-a -> irreducible; end; definition let F be non quadratic_complete non 2-characteristic polynomial_disjoint Field; let a be non square Element of F; func sqrt a -> Element of embField(canHomP X^2-a) equals :: FIELD_9:def 21 KrRootP(X^2-a); end; registration let F be non quadratic_complete non 2-characteristic polynomial_disjoint Field; let a be non square Element of F; cluster sqrt a -> non zero F-algebraic; end; registration let F be non quadratic_complete non 2-characteristic polynomial_disjoint Field; let a be non square Element of F; cluster embField(canHomP X^2-a) -> (FAdj(F,{sqrt a}))-extending; end; registration let F be non quadratic_complete non 2-characteristic polynomial_disjoint Field; let a be non square Element of F; cluster sqrt a -> (FAdj(F,{sqrt a}))-membered non F-membered; end; reserve F for non 2-characteristic non quadratic_complete polynomial_disjoint Field; theorem :: FIELD_9:53 for a being non square Element of F holds (sqrt a) * (sqrt a) = a; theorem :: FIELD_9:54 for a being non square Element of F holds MinPoly(sqrt a,F) = X^2-a; theorem :: FIELD_9:55 for a being non square Element of F holds deg(FAdj(F,{sqrt a}),F) = 2; theorem :: FIELD_9:56 for a being non square Element of F holds (X-(sqrt a)) *' (X+(sqrt a)) = X^2-a; theorem :: FIELD_9:57 for a being non square Element of F holds Roots(FAdj(F,{sqrt a}),X^2-a) = { sqrt a, -(sqrt a) }; theorem :: FIELD_9:58 for a being non square Element of F holds FAdj(F,{sqrt a}) is SplittingField of X^2-a; theorem :: FIELD_9:59 for a being non square Element of F holds {1.F, sqrt a} is Basis of VecSp(FAdj(F,{sqrt a}),F); theorem :: FIELD_9:60 for a being non square Element of F holds the carrier of FAdj(F,{sqrt a}) = the set of all y + @(sqrt a) * z where y,z is F-membered Element of FAdj(F,{sqrt a}); theorem :: FIELD_9:61 for a being non square Element of F for a1,a2,b1,b2 being F-membered Element of FAdj(F,{sqrt a}) st a1 + @(sqrt a) * b1 = a2 + @(sqrt a) * b2 holds a1 = a2 & b1 = b2; begin :: Splittingfields for quadratic Polynomials definition let F be non 2-characteristic Field; let p be quadratic Element of the carrier of Polynom-Ring F; attr p is DC-square means :: FIELD_9:def 22 DC p is square; end; registration let F be non 2-characteristic Field; cluster monic DC-square for quadratic Element of the carrier of Polynom-Ring F; end; registration let F be non quadratic_complete non 2-characteristic Field; cluster monic non DC-square for quadratic Element of the carrier of Polynom-Ring F; end; registration let F be non quadratic_complete non 2-characteristic Field; let p be non DC-square quadratic Element of the carrier of Polynom-Ring F; cluster DC p -> non square; end; registration let F be non quadratic_complete non 2-characteristic Field; let p be non DC-square quadratic Element of the carrier of Polynom-Ring F; cluster X^2-(DC p) -> irreducible; end; registration let F be non 2-characteristic Field; let p be DC-square quadratic Element of the carrier of Polynom-Ring F; cluster X^2-(DC p) -> reducible; end; theorem :: FIELD_9:62 for F being non 2-characteristic Field, p being quadratic Element of the carrier of Polynom-Ring F holds F is SplittingField of p iff DC p is square; registration let F be non 2-characteristic non quadratic_complete polynomial_disjoint Field, p be non DC-square quadratic Element of the carrier of Polynom-Ring F; cluster sqrt(DC p) -> non zero F-algebraic; end; definition let F be non 2-characteristic non quadratic_complete polynomial_disjoint Field, p be non DC-square quadratic Element of the carrier of Polynom-Ring F; func RootDC p -> Element of FAdj(F,{sqrt(DC p)}) equals :: FIELD_9:def 23 sqrt(DC p); end; definition let F be non 2-characteristic non quadratic_complete polynomial_disjoint Field, p be non DC-square quadratic Element of the carrier of Polynom-Ring F; func Root1 p -> Element of FAdj(F,{sqrt(DC p)}) equals :: FIELD_9:def 24 (-@(p.1,FAdj(F,{sqrt(DC p)})) + (RootDC p)) * (2 '*' @(p.2,FAdj(F,{sqrt(DC p)})))"; func Root2 p -> Element of FAdj(F,{sqrt(DC p)}) equals :: FIELD_9:def 25 (-@(p.1,FAdj(F,{sqrt(DC p)})) - (RootDC p)) * (2 '*' @(p.2,FAdj(F,{sqrt(DC p)})))"; end; reserve p for non DC-square quadratic Element of the carrier of Polynom-Ring F; theorem :: FIELD_9:63 (RootDC p) * (RootDC p) = DC p; theorem :: FIELD_9:64 for a being non zero Element of FAdj(F,{sqrt(DC p)}), b,c being Element of FAdj(F,{sqrt(DC p)}) st p = <%c,b,a%> holds Root1 p = (-b + (RootDC p)) * (2 '*' a)" & Root2 p = (-b - (RootDC p)) * (2 '*' a)"; theorem :: FIELD_9:65 p = @(LC p,FAdj(F,{sqrt(DC p)})) * (X-(Root1 p)) *' (X-(Root2 p)); theorem :: FIELD_9:66 Roots(FAdj(F,{sqrt(DC p)}),p) = { Root1 p, Root2 p }; theorem :: FIELD_9:67 Root1 p <> Root2 p; theorem :: FIELD_9:68 deg(FAdj(F,{sqrt(DC p)}),F) = 2; theorem :: FIELD_9:69 FAdj(F,{sqrt(DC p)}) is SplittingField of p; begin :: Quadratic Extensions definition let F be Field, E be FieldExtension of F; attr E is F-quadratic means :: FIELD_9:def 26 deg(E,F) = 2; end; registration let F be non quadratic_complete polynomial_disjoint non 2-characteristic Field; cluster F-quadratic for FieldExtension of F; end; registration let F be Field; cluster F-quadratic -> F-finite for FieldExtension of F; end; registration let F be non quadratic_complete non 2-characteristic polynomial_disjoint Field; let a be non square Element of F; cluster FAdj(F,{sqrt a}) -> F-quadratic; end; theorem :: FIELD_9:70 for F being Field for a,b being Element of F st b^2 = a holds eval(X^2-a,b) = 0.F; theorem :: FIELD_9:71 for F being non 2-characteristic Field, E being FieldExtension of F for a being Element of F st not(ex b being Element of F st a = b^2) for b being Element of E st b^2 = a holds FAdj(F,{b}) is SplittingField of X^2-a & deg(FAdj(F,{b}),F) = 2; theorem :: FIELD_9:72 for F being non 2-characteristic Field for E being FieldExtension of F holds deg(E,F) = 2 iff (ex a being Element of F st not(ex b being Element of F st a = b^2) & ex b being Element of E st a = b^2 & E == FAdj(F,{b})); theorem :: FIELD_9:73 for E being FieldExtension of F holds E is F-quadratic iff ex a being non square Element of F st E,FAdj(F,{sqrt a}) are_isomorphic_over F;