:: 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;