1(* ------------------------------------------------------------------------- *) 2(* Finite Field: Minimal Polynomial *) 3(* ------------------------------------------------------------------------- *) 4 5(*===========================================================================*) 6 7(* add all dependent libraries for script *) 8open HolKernel boolLib bossLib Parse; 9 10(* declare new theory at start *) 11val _ = new_theory "ffMinimal"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16 17(* val _ = load "jcLib"; *) 18open jcLib; 19 20(* val _ = load "SatisfySimps"; (* for SatisfySimps.SATISFY_ss *) *) 21 22(* Get dependent theories local *) 23(* val _ = load "ffUnityTheory"; *) 24open ffBasicTheory; 25open ffAdvancedTheory; 26open ffPolyTheory; 27open ffUnityTheory; 28 29open VectorSpaceTheory; 30open SpanSpaceTheory; 31open LinearIndepTheory; 32open FiniteVSpaceTheory; 33 34(* open dependent theories *) 35open arithmeticTheory pred_setTheory listTheory; 36 37(* Get dependent theories in lib *) 38(* (* val _ = load "helperNumTheory"; -- in monoidTheory *) *) 39open helperNumTheory helperSetTheory helperListTheory; 40 41(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) 42(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) 43open dividesTheory gcdTheory; 44 45(* (* val _ = load "groupInstancesTheory"; -- in ringInstancesTheory *) *) 46(* (* val _ = load "ringInstancesTheory"; *) *) 47(* (* val _ = load "fieldInstancesTheory"; *) *) 48open monoidTheory groupTheory ringTheory fieldTheory; 49open monoidOrderTheory groupOrderTheory fieldOrderTheory; 50open subgroupTheory; 51open groupInstancesTheory ringInstancesTheory fieldInstancesTheory; 52 53(* Get polynomial theory of Ring *) 54(* (* val _ = load "polyFieldModuloTheory"; *) *) 55open polynomialTheory polyWeakTheory polyRingTheory polyDivisionTheory polyBinomialTheory; 56open polyMonicTheory polyEvalTheory; 57open polyDividesTheory; 58open polyRootTheory; 59 60(* (* val _ = load "polyFieldDivisionTheory"; *) *) 61open fieldMapTheory; 62open polyFieldTheory; 63open polyFieldDivisionTheory; 64open polyFieldModuloTheory; 65open polyIrreducibleTheory; 66 67(* (* val _ = load "ringBinomialTheory"; *) *) 68open ringBinomialTheory; 69open ringDividesTheory; 70open ringIdealTheory; 71open ringUnitTheory; 72 73 74(* ------------------------------------------------------------------------- *) 75(* Finite Field Minimal Polynomial Documentation *) 76(* ------------------------------------------------------------------------- *) 77(* Overload: 78 ebasis = element_powers_basis r 79 p <o> b = \(p:'a poly) (b:'a list). VectorSum r.sum (MAP2 r.prod.op p b) 80 subfield_monics x = subfield_monics_of_element r s x 81 Minimals x = poly_minimals r s x 82 minimal x = poly_minimal r s x 83 degree x = poly_deg (r:'a ring) (poly_minimal (r:'a ring) (s:'a ring) x) 84 degree_ x = poly_deg (r_:'b ring) (poly_minimal (r_:'b ring) (s_:'b ring) x) 85 pfmonic = poly_monic (PF r) 86 pfipoly = irreducible (PolyRing (PF r)) 87 pfppideal = principal_ideal (PolyRing r) 88 sideal = set_to_ideal r 89*) 90(* Definitions and Theorems (# are exported): 91 92 Minimal Polynomial via Linear Independence: 93 element_powers_basis_def |- !r x n. ebasis x n = GENLIST (\j. x ** j) (SUC n) 94 element_powers_basis_0 |- !r x. ebasis x 0 = [#1] 95 element_powers_basis_suc |- !r x. ebasis x (SUC n) = SNOC (x ** SUC n) (ebasis x n) 96 element_powers_basis_is_basis |- !r. Ring r ==> !x. x IN R ==> !n. basis r.sum (ebasis x n) 97 element_powers_basis_length |- !n. LENGTH (ebasis x n) = SUC n 98 element_powers_basis_dependent |- !r s. FiniteField r /\ s <<= r ==> !x. x IN R ==> 99 ~LinearIndepBasis s r.sum $* (ebasis x (dim s r.sum $* )) 100 element_powers_basis_dim_dep |- !r. FiniteField r ==> !x. x IN R ==> 101 ~LinearIndepBasis (PF r) r.sum $* (ebasis x (dim (PF r) r.sum $* )) 102 103 stick_is_weak |- !r p n. p IN sticks r n ==> weak p 104 subfield_poly_weak_is_weak |- !r s. s <<= r ==> !p. Weak s p ==> weak p 105 subfield_stick_is_weak |- !r s. s <<= r ==> !p n. p IN sticks s n ==> weak p 106 subfield_sticks_vsum_eq_eval |- !r s. s <<= r ==> !p n. p IN sticks s (SUC n) ==> 107 !x. x IN R ==> (p <o> ebasis x n = eval p x) 108 subfield_poly_of_element |- !r s. FiniteField r /\ s <<= r ==> 109 !x. x IN R ==> ?p. Poly s p /\ 0 < deg p /\ root p x 110 subfield_monic_of_element |- !r s. FiniteField r /\ s <<= r ==> 111 !x. x IN R ==> ?p. poly_monic s p /\ 0 < deg p /\ root p x 112 113 Minimal Polynomial in Subfield: 114 subfield_monics_of_element_def |- !r s x. subfield_monics x = 115 {p | poly_monic s p /\ 0 < deg p /\ root p x} 116 poly_minimals_def |- !r s x. Minimals x = 117 preimage deg (subfield_monics x) (MIN_SET (IMAGE deg (subfield_monics x))) 118 poly_minimal_def |- !r s x. minimal x = CHOICE (Minimals x) 119 subfield_monics_of_element_member |- !r s x p. p IN subfield_monics x <=> 120 poly_monic s p /\ 0 < deg p /\ root p x 121 subfield_monics_of_element_nonempty |- !r s. FiniteField r /\ s <<= r ==> 122 !x. x IN R ==> subfield_monics x <> {} 123 poly_minimals_member |- !p. p IN Minimals x <=> poly_monic s p /\ 0 < deg p /\ root p x /\ 124 (deg p = MIN_SET (IMAGE deg (subfield_monics x))) 125 poly_minimals_deg_pos |- !r s. FiniteField r /\ s <<= r ==> 126 !x. x IN R ==> 0 < MIN_SET (IMAGE deg (subfield_monics x)) 127 poly_minimals_has_monoimal_condition |- !r s. FiniteField r /\ s <<= r ==> !x. x IN R ==> 128 !p. poly_monic s p /\ (deg p = 1) /\ root p x ==> p IN Minimals x 129 poly_minimals_nonempty |- !r s. FiniteField r /\ s <<= r ==> !x. x IN R ==> Minimals x <> {} 130 poly_minimal_property |- !r s. FiniteField r /\ s <<= r ==> !x. x IN R ==> 131 minimal x IN subfield_monics x /\ 132 (degree x = MIN_SET (IMAGE deg (subfield_monics x))) 133 poly_minimal_subfield_property |- !r s. FiniteField r /\ s <<= r ==> !x. x IN R ==> 134 poly_monic s (minimal x) /\ 0 < degree x /\ root (minimal x) x 135 poly_minimal_spoly |- !r s. FiniteField r /\ s <<= r ==> !x. x IN R ==> Poly s (minimal x) 136 poly_minimal_poly |- !r s. FiniteField r /\ s <<= r ==> !x. x IN R ==> poly (minimal x) 137 poly_minimal_deg_pos |- !r s. FiniteField r /\ s <<= r ==> !x. x IN R ==> 0 < degree x 138 poly_minimal_not_unit |- !r s. FiniteField r /\ s <<= r ==> !x. x IN R ==> ~upoly (minimal x) 139 poly_minimal_ne_poly_one |- !r s. FiniteField r /\ s <<= r ==> !x. x IN R ==> minimal x <> |1| 140 poly_minimal_ne_poly_zero |- !r s. FiniteField r /\ s <<= r ==> !x. x IN R ==> minimal x <> |0| 141 poly_minimal_has_element_root |- !r s. FiniteField r /\ s <<= r ==> !x. x IN R ==> root (minimal x) x 142 poly_minimal_monic |- !r s. FiniteField r /\ s <<= r ==> !x. x IN R ==> monic (minimal x) 143 poly_minimal_pmonic |- !r s. FiniteField r /\ s <<= r ==> !x. x IN R ==> pmonic (minimal x) 144 poly_minimal_divides_subfield_poly |- !r s. FiniteField r /\ s <<= r ==> !x. x IN R ==> 145 !p. Poly s p /\ root p x ==> minimal x pdivides p 146 poly_minimal_divides_subfield_poly_alt 147 |- !r s. FiniteField r /\ s <<= r ==> 148 !p x. Poly s p /\ x IN roots p ==> minimal x pdivides p 149 poly_minimal_divides_subfield_poly_iff 150 |- !r s. FiniteField r /\ s <<= r ==> !x. x IN R ==> 151 !p. Poly s p ==> (root p x <=> minimal x pdivides p) 152 poly_minimal_eval_congruence |- !r s. FiniteField r /\ s <<= r ==> !x. x IN R ==> 153 !p q. Poly s p /\ Poly s q ==> 154 ((eval p x = eval q x) <=> (p % minimal x = q % minimal x)) 155 poly_minimal_divides_unity_order |- !r s. FiniteField r /\ s <<= r ==> 156 !x. x IN R ==> minimal x pdivides unity (forder x) 157 158 Minimal Polynomial is unique and irreducible: 159 poly_minimals_sing |- !r s. FiniteField r /\ s <<= r ==> !x. x IN R ==> SING (Minimals x) 160 poly_minimal_zero |- !r s. FiniteField r /\ s <<= r ==> (minimal #0 = X) 161 poly_minimal_one |- !r s. FiniteField r /\ s <<= r ==> (minimal #1 = X - |1|) 162 poly_minimal_eq_X |- !r s. FiniteField r /\ s <<= r ==> !x. x IN R ==> ((minimal x = X) <=> (x = #0)) 163 poly_minimal_subfield_irreducible |- !r s. FiniteField r /\ s <<= r ==> !x. x IN R ==> IPoly s (minimal x) 164 165 Minimal Polynomial of Prime Field: 166 prime_field_stick_is_weak |- !r. FiniteField r ==> !p n. p IN sticks (PF r) n ==> weak p 167 168 vsum_element_powers_basis_eq_eval |- !r. FiniteField r ==> !p n. p IN sticks (PF r) (SUC n) ==> 169 !x. x IN R ==> (p <o> ebasis x n = eval p x) 170 poly_prime_field_with_root_exists |- !r. FiniteField r ==> !x. x IN R ==> 171 ?p. pfpoly p /\ 0 < deg p /\ root p x 172 poly_prime_field_monic_with_root_exists |- !r. FiniteField r ==> !x. x IN R ==> 173 ?p. pfmonic p /\ 0 < deg p /\ root p x 174 175 Ideals of Polynomial Ring: 176 poly_ring_zero_ideal |- !r. Ring r ==> !p. poly p ==> ((pfppideal p = pfppideal |0|) <=> (p = |0|)) 177 poly_ring_ideal_gen_monic |- !r. Field r ==> !i. i << PolyRing r /\ i <> pfppideal |0| ==> 178 ?p. monic p /\ (i = pfppideal p) 179 poly_field_principal_ideal_equal |- !r. Field r ==> !p q. poly p /\ poly q ==> 180 ((pfppideal p = pfppideal q) <=> ?u. poly u /\ upoly u /\ (p = u * q)) 181 poly_ring_ideal_monic_gen_unique |- !r. Field r ==> !p q. monic p /\ monic q /\ 182 (pfppideal p = pfppideal q) ==> (p = q) 183 184 The Ideal of Polynomials sharing a root: 185 set_to_ideal_def |- !r s. sideal s = 186 <|carrier := s; 187 sum := <|carrier := s; op := $+; id := #0|>; 188 prod := <|carrier := s; op := $*; id := #1|> 189 |> 190 poly_root_poly_ideal |- !r. Ring r ==> !z. z IN R ==> 191 set_to_ideal (PolyRing r) {p | poly p /\ root p z} << PolyRing r 192 193*) 194 195(* ------------------------------------------------------------------------- *) 196(* Helper Theorems *) 197(* ------------------------------------------------------------------------- *) 198 199(* ------------------------------------------------------------------------- *) 200(* Minimal Polynomial via Linear Independence *) 201(* ------------------------------------------------------------------------- *) 202 203(* 204Timothy Murphy -- Finite Field (course notes) p.29, Posposition 8. 205 206Theorem: Let F be a finite field with prime subfield P. 207Each element of a IN F is a root of a unique irreducible polynomial m(x) over P. 208If |F| = p**n, then deg m(x) <= n. 209For each polynomial f(x) over P, f(a) = 0 iff m(x) | f(x) 210Proof: 211Let a IN F, and n = Dim (PF) F (or F = char r ** n). Then (n+1) elements: 212 1, a, a**2, a**3, ...., a**n 213must be linearly dependent, i.e. c_0 + c_1 a + c_2 a **2 + ... + c_n a**n = 0 214for some c_j IN P (not all zero). In other words, a is a root of the polynomial 215 f(x) = c_0 + c_1 x + c_2 x **2 + ... + c_n x**n 216Now, let m(x) be the polynomial of smallest degree > 0 satisifed by a. 217Then deg m <= deg f <= n. 218Also, m(x) must be irreducible. For if m(x) = u(x) v(x) 219Then 0 = m(a) = u(a) v(a) ==> u(a) = 0 or v(a) = 0 since F is a field. 220But this contradicts the minimality of m(x). 221Finally, suppose f(x) in P(x) has f(a) = 0. 222Divide f(x) by m(x): f(x) = m(x) q(x) + r(x) where deg r(x) < m(x) 223Then r(a) = f(a) - m(a)q(a) = 0 224and so r(x) = 0 by the minimality of m(x), i.e. m(x) | f(x). 225This last result shows in particular that m(x) is the only irreducible polynomial 226(up to a scalar multiple) satisfied by a. 227*) 228 229(* Define a basis compose of element powers *) 230val element_powers_basis_def = Define` 231 element_powers_basis (r:'a ring) (x:'a) n = GENLIST (\j. x ** j) (SUC n) 232`; 233(* overload on element powers basis *) 234val _ = overload_on("ebasis", ``element_powers_basis r``); 235 236(* Overload the vector sum of ring prod group between poly and base. *) 237val _ = overload_on("<o>", ``\(p:'a poly) (b:'a list). VectorSum r.sum (MAP2 r.prod.op p b)``); 238val _ = set_fixity "<o>" (Infixl 500); (* same as + in arithmeticScript.sml *) 239 240(* Theorem: !x. ebasis x 0 = [#1] *) 241(* Proof: 242 ebasis x 0 243 = GENLIST (\j. x ** j) (SUC 0) by element_powers_basis_def 244 = SNOC ((\j. x ** j) 0) (GENLIST (\j. x ** j) 0) by GENLIST 245 = SNOC ((\j. x ** j) 0) [] by GENLIST 246 = [((\j. x ** j) 0)] by SNOC 247 = [x ** 0] by application 248 = [#1] by ring_exp_0 249*) 250val element_powers_basis_0 = store_thm( 251 "element_powers_basis_0", 252 ``!r:'a field. !x. ebasis x 0 = [#1]``, 253 rw[element_powers_basis_def]); 254 255(* Theorem: ebasis x (SUC n) = SNOC (x ** (SUC n)) (ebasis x n) *) 256(* Proof: 257 ebasis x (SUC n) 258 = GENLIST (\j. x ** j) (SUC (SUC n)) by element_powers_basis_def 259 = SNOC ((\j. x ** j) (SUC n)) (GENLIST (\j. x ** j) (SUC n)) by GENLIST 260 = SNOC ((\j. x ** j) (SUC n)) (ebasis x n) by element_powers_basis_def 261 = SNOC (x ** (SUC n)) (ebasis x n) by application 262*) 263val element_powers_basis_suc = store_thm( 264 "element_powers_basis_suc", 265 ``!r:'a field. !x. ebasis x (SUC n) = SNOC (x ** (SUC n)) (ebasis x n)``, 266 rpt strip_tac >> 267 `!n. (\j. x ** j) n = x ** n` by rw[] >> 268 metis_tac[element_powers_basis_def, GENLIST]); 269 270(* Theorem: Ring r ==> !x. x IN R ==> !n. basis r.sum (ebasis x n) *) 271(* Proof: 272 basis r.sum (ebasis x n) 273 <=> !y. MEM y (ebasis x n) ==> y IN r.sum.carrier by basis_member 274 <=> !y. MEM y (ebasis x n) ==> y IN R by ring_carriers 275 <=> !y. MEM y (GENLIST (\j. x ** j) (SUC n)) ==> y IN R by element_powers_basis_def 276 <=> !y. ?m. m < SUC n /\ (y = (\j. x ** j) m) ==> y IN R by MEM_GENLIST 277 <=> !y. j < SUC n ==> x ** j IN R by application 278 <=> T by ring_exp_element 279*) 280val element_powers_basis_is_basis= store_thm( 281 "element_powers_basis_is_basis", 282 ``!r:'a ring. Ring r ==> !x. x IN R ==> !n. basis r.sum (ebasis x n)``, 283 rw[element_powers_basis_def, basis_member, MEM_GENLIST] >> 284 rw[]); 285 286(* Theorem: LENGTH (ebasis x n) = SUC n *) 287(* Proof: 288 LENGTH (ebasis x n) 289 = LENGTH (GENLIST (\j. x ** j) (SUC n)) by element_powers_basis_def 290 = SUC n by LENGTH_GENLIST 291*) 292val element_powers_basis_length = store_thm( 293 "element_powers_basis_length", 294 ``!n. LENGTH (ebasis x n) = SUC n``, 295 rw[element_powers_basis_def]); 296 297(* Theorem: FiniteField r ==> !s:'a field. s <<= r ==> !x. x IN R ==> 298 ~LinearIndepBasis s r.sum $* (ebasis x (dim s r.sum $* ) *) 299(* Proof: 300 Let n = dim s r.sum $*. 301 Since FiniteField r 302 ==> FiniteVSpace s r.sum $* by finite_subfield_is_finite_vspace_scalar 303 and basis r.sum (ebasis x n) by element_powers_basis_is_basis, field_is_ring 304 and n < LENGTH (ebasis x n) by element_powers_basis_length, n < SUC n 305 Hence ~LinearIndepBasis s r.sum $* (ebasis x n) 306 by finite_vspace_basis_dep 307*) 308val element_powers_basis_dependent = store_thm( 309 "element_powers_basis_dependent", 310 ``!r:'a field. FiniteField r ==> !s:'a field. s <<= r ==> !x. x IN R ==> 311 ~LinearIndepBasis s r.sum $* (ebasis x (dim s r.sum $* ))``, 312 rpt (stripDup[FiniteField_def]) >> 313 qabbrev_tac `n = dim s r.sum $*` >> 314 `FiniteVSpace s r.sum $*` by rw[finite_subfield_is_finite_vspace_scalar] >> 315 `basis r.sum (ebasis x n)` by rw[element_powers_basis_is_basis] >> 316 `n < LENGTH (ebasis x n)` by rw[element_powers_basis_length] >> 317 metis_tac[finite_vspace_basis_dep]); 318 319(* Theorem: FiniteField r ==> !x. x IN R ==> 320 ~LinearIndepBasis (PF r) r.sum $* (ebasis x (dim (PF r) r.sum $* )) *) 321(* Proof: 322 Let n = dim (PF r) r.sum $*. 323 Since FiniteField r 324 ==> FiniteVSpace (PF r) r.sum $* by finite_field_is_finite_vspace 325 and basis r.sum (ebasis x n) by element_powers_basis_is_basis, field_is_ring 326 and n < LENGTH (ebasis x n) by element_powers_basis_length, n < SUC n 327 Hence ~LinearIndepBasis (PF r) r.sum $* (ebasis x n) 328 by finite_vspace_basis_dep 329*) 330val element_powers_basis_dim_dep = store_thm( 331 "element_powers_basis_dim_dep", 332 ``!r:'a field. FiniteField r ==> !x. x IN R ==> 333 ~LinearIndepBasis (PF r) r.sum $* (ebasis x (dim (PF r) r.sum $* ))``, 334 rpt (stripDup[FiniteField_def]) >> 335 qabbrev_tac `n = dim (PF r) r.sum $*` >> 336 `FiniteVSpace (PF r) r.sum $*` by rw[finite_field_is_finite_vspace] >> 337 `basis r.sum (ebasis x n)` by rw[element_powers_basis_is_basis] >> 338 `n < LENGTH (ebasis x n)` by rw[element_powers_basis_length] >> 339 metis_tac[finite_vspace_basis_dep]); 340 341(* Theorem: !n. p IN sticks r n ==> weak p *) 342(* Proof: 343 By induction on n. 344 Base case: !p. p IN sticks r 0 ==> weak p 345 p IN sticks r 0 346 ==> p IN {[]} by sticks_0 347 ==> p = [] by IN_SING 348 and weak [] = T by weak_of_zero 349 Step case: !p. p IN sticks r n ==> weak p ==> 350 !p. p IN sticks r (SUC n) ==> weak p 351 p IN sticks r (SUC n) 352 ==> ?h t. h IN R /\ t IN sticks r n /\ (p = h::t) by stick_cons 353 ==> h IN R /\ weak t /\ (p = h::t) by induction hypothesis 354 ==> weak p by weak_cons 355*) 356val stick_is_weak = store_thm( 357 "stick_is_weak", 358 ``!(r:'a field) p n. p IN sticks r n ==> weak p``, 359 strip_tac >> 360 Induct_on `n` >- 361 rw[sticks_0] >> 362 metis_tac[stick_cons, weak_cons]); 363 364(* Theorem: s <<= r ==> !p. Weak s p ==> weak p *) 365(* Proof: 366 By induction on p. 367 Base case: Weak s [] ==> weak [] 368 True by weak_of_zero. 369 Step case: Weak s p ==> weak p ==> !h. Weak s (h::p) ==> weak (h::p) 370 Weak s (h::p) 371 ==> h IN s.carrier /\ Weak s p by weak_cons 372 ==> h IN s.carrier /\ weak s p by induction hypothesis 373 ==> h IN R /\ weak s p by subfield_element 374 ==> weak (h::p) by weak_cons 375*) 376val subfield_poly_weak_is_weak = store_thm( 377 "subfield_poly_weak_is_weak", 378 ``!(r s):'a field. s <<= r ==> !p. Weak s p ==> weak p``, 379 rpt strip_tac >> 380 Induct_on `p` >- 381 rw[] >> 382 rw[] >> 383 metis_tac[subfield_element]); 384 385(* Theorem: s <<= r ==> !p n. p IN sticks s n ==> weak p *) 386(* Proof: 387 Since p IN sticks s n 388 ==> Weak s p by stick_is_weak 389 ==> weak p by subfield_poly_weak_is_weak 390*) 391val subfield_stick_is_weak = store_thm( 392 "subfield_stick_is_weak", 393 ``!(r s):'a field. s <<= r ==> !p n. p IN sticks s n ==> weak p``, 394 metis_tac[stick_is_weak, subfield_poly_weak_is_weak]); 395 396(* Theorem: s <<= r ==> !p n. p IN sticks s (SUC n) ==> 397 !x. x IN R ==> (p <o> (ebasis x n) = eval p x) *) 398(* Proof: 399 By induction on n. 400 Base case: !p. p IN sticks s (SUC 0) ==> 401 !x. x IN R ==> (p <o> ebasis x 0 = eval p x) 402 p IN sticks s (SUC 0) 403 ==> p IN sticks s 1 by ONE 404 ==> ?c. c IN B /\ (p = [c]) by sticks_1_member 405 Note c IN R by subfield_element 406 Also ebasis x 0 = [#1] by element_powers_basis_0 407 p <o> ebasis x 0 408 = VectorSum r.sum (MAP2 $* [c] [#1]) by notation, p = [c], ebasis x 0 = [#1] 409 = VectorSum r.sum [c * #1] by MAP2 410 = VectorSum r.sum [c] by ring_mult_rone 411 = c + (VectorSum r.sum []) by vsum_cons 412 = c + #0 by vsum_nil 413 = c by ring_add_rzero 414 = eval [c] x by poly_eval_const 415 Step case: !p. p IN sticks s (SUC (SUC n)) ==> 416 !x. x IN R ==> (p <o> ebasis x (SUC n) = eval p x) 417 p IN sticks s (SUC (SUC n)) 418 ==> ?h t. h IN B /\ t IN sticks s (SUC n) /\ (p = SNOC h t) by stick_snoc 419 Note LENGTH t = SUC n by stick_length 420 Also ebasis x (SUC n) = SNOC (x ** (SUC n)) (ebasis x n) by element_powers_basis_suc 421 and h IN R by subfield_element 422 and weak t by subfield_stick_is_weak 423 and eval t x IN R by weak_eval_element 424 p <o> (ebasis x (SUC n))) 425 = (SNOC h t) <o> (SNOC (x ** (SUC n)) (ebasis x n)) by above 426 = h * (x ** SUC n) + t <o> (ebasis x n) by vsum_stick_snoc 427 = h * (x ** SUC n) + eval t x by induction hypothesis 428 = eval t x + h * x ** LENGTH t by ring_add_comm 429 = eval (SNOC h t) x by weak_eval_snoc 430 = eval p x by p = SNOC h t 431*) 432val subfield_sticks_vsum_eq_eval = store_thm( 433 "subfield_sticks_vsum_eq_eval", 434 ``!(r s):'a field. s <<= r ==> !p n. p IN sticks s (SUC n) ==> 435 !x. x IN R ==> (p <o> (ebasis x n) = eval p x)``, 436 ntac 3 strip_tac >> 437 Induct_on `n` >| [ 438 rw[] >> 439 `?c. c IN B /\ (p = [c])` by rw[GSYM sticks_1_member] >> 440 `c IN R` by metis_tac[subfield_element] >> 441 `ebasis x 0 = [#1]` by rw[element_powers_basis_0] >> 442 rw[vsum_cons, vsum_nil], 443 rpt strip_tac >> 444 `?h t. h IN B /\ t IN sticks s (SUC n) /\ (p = SNOC h t)` by rw[GSYM stick_snoc] >> 445 `ebasis x (SUC n) = SNOC (x ** (SUC n)) (ebasis x n)` by rw_tac std_ss[element_powers_basis_suc] >> 446 `VSpace s r.sum $*` by rw[field_is_vspace_over_subfield] >> 447 `basis r.sum (ebasis x n)` by rw[element_powers_basis_is_basis] >> 448 `LENGTH (ebasis x n) = SUC n` by rw[element_powers_basis_length] >> 449 `x ** SUC n IN R /\ (R = r.sum.carrier)` by rw[] >> 450 `h IN R` by metis_tac[subfield_element] >> 451 `weak t` by metis_tac[subfield_stick_is_weak] >> 452 `p <o> (ebasis x (SUC n)) = h * (x ** SUC n) + eval t x` by metis_tac[vsum_stick_snoc] >> 453 `_ = h * x ** LENGTH t + eval t x` by metis_tac[stick_length] >> 454 `_ = eval t x + h * x ** LENGTH t` by rw[ring_add_comm] >> 455 `_ = eval p x` by rw[weak_eval_snoc] >> 456 rw[] 457 ]); 458 459(* Theorem: FiniteField r ==> !s. s <<= r ==> !x. x IN R ==> ?p. Poly s p /\ 0 < deg p /\ root p x *) 460(* Proof: 461 Let n = dim s r.sum $*, b = ebasis x n. 462 Then ~LinearIndepBasis s r.sum $* b by element_powers_basis_dependent 463 Note basis r.sum b by element_powers_basis_is_basis 464 and LENGTH b = SUC n by element_powers_basis_length 465 and s.sum.id = #0 by subfield_ids 466 Hence by LinearIndepBasis_def, 467 ?q. q IN sticks s (SUC n) /\ 468 ~(q <o> b) = #0) <=> !k. k < SUC n ==> (EL k q = #0)) [1] 469 470 Note VSpace s r.sum $* by subfield_is_vspace_scalar 471 and !k. k < SUC n ==> (EL k q = #0)) ==> (q <o> b) = #0) by vspace_stick_zero 472 Thus ?k. k < SUC n /\ (EL k p <> #0) /\ (q <o> b) = #0) by [1] 473 Now Weak s q by stick_is_weak 474 and LENGTH q = SUC n by stick_length 475 so ~(zero_poly s q) by zero_poly_element, EL k q <> #0 476 Let p = poly_chop s q 477 Then Poly s p by poly_chop_weak_poly 478 and ~(zero_poly s p) by zero_poly_eq_zero_poly_chop 479 thus p <> (PolyRing s).sum.id by zero_poly_eq_poly_zero 480 or p <> |0| by subring_poly_ids, subfield_is_subring 481 Also eval p x = eval (poly_chop s q) x 482 = eval (chop q) x by subring_poly_chop 483 = eval q x by poly_eval_chop 484 = q <o> b by subfield_sticks_vsum_eq_eval 485 = #0 by above 486 Hence root p x by poly_root_def 487 with 0 < deg p by poly_nonzero_with_root_deg_pos 488*) 489val subfield_poly_of_element = store_thm( 490 "subfield_poly_of_element", 491 ``!(r s):'a field. FiniteField r /\ s <<= r ==> !x. x IN R ==> ?p. Poly s p /\ 0 < deg p /\ root p x``, 492 rpt (stripDup[FiniteField_def]) >> 493 qabbrev_tac `n = dim s r.sum $*` >> 494 qabbrev_tac `b = ebasis x n` >> 495 `~LinearIndepBasis s r.sum $* b` by rw[element_powers_basis_dependent, Abbr`n`, Abbr`b`] >> 496 `basis r.sum b` by rw[element_powers_basis_is_basis, Abbr`b`] >> 497 `LENGTH b = SUC n` by rw[element_powers_basis_length, Abbr`b`] >> 498 `s.sum.id = #0` by rw[subfield_ids] >> 499 `?q. q IN sticks s (SUC n) /\ 500 ~((q <o> b = #0) <=> !k. k < SUC n ==> (EL k q = #0))` by metis_tac[LinearIndepBasis_def] >> 501 `VSpace s r.sum $*` by rw[subfield_is_vspace_scalar] >> 502 `?k. k < SUC n /\ (EL k q <> #0) /\ (q <o> b = #0)` by metis_tac[vspace_stick_zero] >> 503 `Weak s q` by metis_tac[stick_is_weak] >> 504 qexists_tac `poly_chop s q` >> 505 `Poly s (poly_chop s q)` by metis_tac[poly_chop_weak_poly] >> 506 `eval q x = #0` by metis_tac[subfield_sticks_vsum_eq_eval] >> 507 `root (chop q) x` by rw[poly_root_def] >> 508 `Ring r /\ Ring s /\ s <= r` by rw[subfield_is_subring] >> 509 `root (poly_chop s q) x` by metis_tac[subring_poly_chop] >> 510 `~(zero_poly s q)` by metis_tac[zero_poly_element, stick_length] >> 511 `~(zero_poly s (poly_chop s q))` by metis_tac[zero_poly_eq_zero_poly_chop] >> 512 `(poly_chop s q) <> |0|` by metis_tac[zero_poly_eq_poly_zero, subring_poly_ids] >> 513 `poly (poly_chop s q)` by metis_tac[subring_poly_poly] >> 514 `0 < deg (poly_chop s q)` by metis_tac[poly_nonzero_with_root_deg_pos] >> 515 rw[]); 516 517(* Theorem: FiniteField r ==> !s. s <<= r ==> !x. x IN R ==> ?p. poly_monic s p /\ 0 < deg p /\ root p x *) 518(* Proof: 519 Since FiniteField r and s <<= r, 520 ==> ?q. Poly q /\ 0 < deg q /\ root q x by subfield_poly_of_element 521 Note poly_zero s = |0| by subring_poly_ids 522 Hence ?u p. Poly s u /\ poly_monic s p /\ 523 (poly_deg s p = poly_deg s q) /\ 524 (p = poly_mult s u q) by poly_monic_mult_by_factor, poly_unit_poly 525 with 0 < deg q = poly_deg s q = poly_deg s p = deg p 526 by subring_poly_deg 527 Since Poly s p by poly_monic_poly 528 Thus poly u /\ poly p /\ poly q /\ by subring_poly_poly 529 (p = u * q) by subring_poly_mult 530 eval p x 531 = (eval u x) * (eval q x) by poly_eval_mult 532 = (eval u x) * #0 by poly_root_def 533 = #0 by poly_eval_element, field_mult_rzero 534 Hence root p x by poly_root_def 535*) 536val subfield_monic_of_element = store_thm( 537 "subfield_monic_of_element", 538 ``!(r s):'a field. FiniteField r /\ s <<= r ==> 539 !x. x IN R ==> ?p. poly_monic s p /\ 0 < deg p /\ root p x``, 540 rpt (stripDup[FiniteField_def]) >> 541 `s <= r` by rw[subfield_is_subring] >> 542 `?q. Poly s q /\ 0 < deg q /\ root q x` by rw_tac std_ss[subfield_poly_of_element] >> 543 `poly_zero s = |0|` by rw[subring_poly_ids] >> 544 `q <> |0|` by rw[poly_deg_pos_nonzero] >> 545 `?u p. Poly s u /\ poly_monic s p /\ 546 (poly_deg s p = poly_deg s q) /\ (p = poly_mult s u q)` by metis_tac[poly_monic_mult_by_factor, poly_unit_poly] >> 547 `0 < deg p` by metis_tac[subring_poly_deg] >> 548 `Poly s p` by rw[] >> 549 `poly u /\ poly p /\ poly q /\ (p = u * q)` by metis_tac[subring_poly_poly, subring_poly_mult] >> 550 `eval p x = (eval u x) * (eval q x)` by rw[poly_eval_mult] >> 551 `_ = (eval u x) * #0` by metis_tac[poly_root_def] >> 552 `_ = #0` by rw[] >> 553 metis_tac[poly_root_def]); 554 555(* ------------------------------------------------------------------------- *) 556(* Minimal Polynomial in Subfield *) 557(* ------------------------------------------------------------------------- *) 558 559(* Define the set of monic subfield polynomials having an element as a root *) 560val subfield_monics_of_element_def = Define ` 561 subfield_monics_of_element (r:'a ring) (s:'a ring) (x: 'a) = 562 { p | poly_monic s p /\ 0 < deg p /\ root p x } 563`; 564 565(* Define the set of minimial polynomials of an element in a subfield *) 566val poly_minimals_def = Define ` 567 poly_minimals (r:'a ring) (s:'a ring) (x: 'a) = 568 preimage deg (subfield_monics_of_element r s x) 569 (MIN_SET (IMAGE deg (subfield_monics_of_element r s x))) 570`; 571 572(* Define minimial polynomial of an element in a subfield *) 573val poly_minimal_def = Define ` 574 poly_minimal (r:'a ring) (s:'a ring) (x: 'a) = CHOICE (poly_minimals r s x) 575`; 576 577(* Define overloads *) 578val _ = overload_on("subfield_monics", ``subfield_monics_of_element r s``); 579val _ = overload_on("Minimals", ``poly_minimals r s``); 580val _ = overload_on("minimal", ``poly_minimal r s``); 581 582(* Overload on the degree of minimal polynomial *) 583val _ = overload_on("degree", ``\x. poly_deg (r:'a ring) (poly_minimal (r:'a ring) (s:'a ring) x)``); 584val _ = overload_on("degree_", ``\x. poly_deg (r_:'b ring) (poly_minimal (r_:'b ring) (s_:'b ring) x)``); 585 586(* 587> subfield_monics_of_element_def; 588val it = |- !r s x. subfield_monics x = {p | poly_monic s p /\ 0 < deg p /\ root p x}: thm 589> poly_minimals_def; 590val it = |- !r s x. Minimals x = preimage deg (subfield_monics x) (MIN_SET (IMAGE deg (subfield_monics x))): thm 591> poly_minimal_def; 592val it = |- !r s x. minimal x = CHOICE (Minimals x): thm 593*) 594 595(* Theorem: p IN subfield_monics x <=> poly_monic s p /\ 0 < deg p /\ root p x *) 596(* Proof: by subfield_monics_of_element_def *) 597val subfield_monics_of_element_member = store_thm( 598 "subfield_monics_of_element_member", 599 ``!(r s):'a field x p:'a poly. p IN subfield_monics x <=> poly_monic s p /\ 0 < deg p /\ root p x``, 600 rw[subfield_monics_of_element_def]); 601 602(* Theorem: FiniteField r ==> !s. s <<= r ==> !x. x IN R ==> subfield_monics x <> {} *) 603(* Proof: by subfield_monic_of_element *) 604val subfield_monics_of_element_nonempty = store_thm( 605 "subfield_monics_of_element_nonempty", 606 ``!(r s):'a field. FiniteField r /\ s <<= r ==> 607 !x. x IN R ==> subfield_monics x <> {}``, 608 metis_tac[subfield_monic_of_element, subfield_monics_of_element_member, MEMBER_NOT_EMPTY]); 609 610(* Theorem: p IN Minimals x <=> poly_monic s p /\ 0 < deg p /\ root p x /\ 611 (deg p = MIN_SET (IMAGE deg (subfield_monics x))) *) 612(* Proof: by preimage_def, poly_minimals_def, subfield_monics_of_element_member *) 613val poly_minimals_member = store_thm( 614 "poly_minimals_member", 615 ``!p. p IN Minimals x <=> poly_monic s p /\ 0 < deg p /\ root p x /\ 616 (deg p = MIN_SET (IMAGE deg (subfield_monics x)))``, 617 rw[preimage_def, poly_minimals_def] >> 618 metis_tac[subfield_monics_of_element_member]); 619 620(* Theorem: FiniteField r ==> !s. s <<= r ==> 621 !x. x IN R ==> 0 < MIN_SET (IMAGE deg (subfield_monics x)) *) 622(* Proof: 623 Let t = subfield_monics x. 624 Then t <> {} by subfield_monics_of_element_nonempty 625 so IMAGE deg t <> {} by IMAGE_EQ_EMPTY 626 Claim: 0 NOTIN (IMAGE deg t), 627 then MIN_SET (IMAGE deg t) <> 0 by MIN_SET_LEM 628 or 0 < MIN_SET (IMAGE deg t) 629 For the claim, prove by contradiction. 630 Let 0 IN (IMAGE deg t), 631 It means there is p IN t /\ deg p = 0 by IN_IMAGE 632 but p IN t ==> 0 < deg p by subfield_monics_of_element_member 633 which is a contradiction. 634*) 635val poly_minimals_deg_pos = store_thm( 636 "poly_minimals_deg_pos", 637 ``!(r s):'a field. FiniteField r /\ s <<= r ==> 638 !x. x IN R ==> 0 < MIN_SET (IMAGE deg (subfield_monics x))``, 639 metis_tac[subfield_monics_of_element_nonempty, IMAGE_EQ_EMPTY, IN_IMAGE, 640 subfield_monics_of_element_member, MIN_SET_LEM, NOT_ZERO_LT_ZERO]); 641 642(* Theorem: FiniteField r ==> !s. s <<= r ==> 643 !x. x IN R ==> !p. Monic s p /\ (deg p = 1) /\ root p x ==> p IN Minimals x *) 644(* Proof: 645 Let t = subfield_monics x. 646 Then t <> {} by subfield_monics_of_element_nonempty 647 so IMAGE deg t <> {} by IMAGE_EQ_EMPTY 648 By poly_minimals_member, need to show: 1 = MIN_SET (IMAGE deg t). 649 Since deg p = 1, 0 < deg p 650 thus p IN t by subfield_monics_of_element_member 651 and deg p IN IMAGE deg t by IN_IMAGE 652 or 1 IN IMAGE deg t by deg p = 1 653 Hence MIN_SET (IMAGE deg t) <= 1 by MIN_SET_LEM 654 But 0 < MIN_SET (IMAGE deg t) by poly_minimals_deg_pos 655 Thus MIN_SET (IMAGE deg t) = 1. 656*) 657val poly_minimals_has_monoimal_condition = store_thm( 658 "poly_minimals_has_monoimal_condition", 659 ``!(r s):'a field. FiniteField r /\ s <<= r ==> 660 !x. x IN R ==> !p. Monic s p /\ (deg p = 1) /\ root p x ==> p IN Minimals x``, 661 rw[poly_minimals_member] >> 662 qabbrev_tac `t = subfield_monics x` >> 663 `t <> {}` by rw[subfield_monics_of_element_nonempty, Abbr`t`] >> 664 `IMAGE deg t <> {}` by rw[IMAGE_EQ_EMPTY] >> 665 `0 < deg p` by decide_tac >> 666 `p IN t` by rw[subfield_monics_of_element_member, Abbr`t`] >> 667 `deg p IN IMAGE deg t` by rw[] >> 668 `MIN_SET (IMAGE deg t) <= 1` by metis_tac[MIN_SET_LEM] >> 669 `0 < MIN_SET (IMAGE deg t)` by metis_tac[poly_minimals_deg_pos] >> 670 decide_tac); 671 672(* Theorem: FiniteField r ==> !s. s <<= r ==> !x. x IN R ==> Minimals x <> {} *) 673(* Proof: 674 Let t = subfield_monics x, y = MIN_SET (IMAGE deg t). 675 Since t <> {} by subfield_monics_of_element_nonempty 676 so IMAGE deg t <> {} by IMAGE_EQ_EMPTY 677 and y IN (IMAGE deg t) by MIN_SET_LEM 678 thus ?p. p IN t /\ (deg p = y) by IN_IMAGE 679 and p IN preimage deg t y by in_preimage 680 or p IN Minimals x by poly_minimals_def 681 Hence Minimals x <> {} by MEMBER_NOT_EMPTY 682*) 683val poly_minimals_nonempty = store_thm( 684 "poly_minimals_nonempty", 685 ``!(r s):'a field. FiniteField r /\ s <<= r ==> !x. x IN R ==> Minimals x <> {}``, 686 rpt (stripDup[FiniteField_def]) >> 687 qabbrev_tac `t = subfield_monics x` >> 688 qabbrev_tac `y = MIN_SET (IMAGE deg t)` >> 689 `t <> {}` by rw[subfield_monics_of_element_nonempty, Abbr`t`] >> 690 `IMAGE deg t <> {}` by rw[IMAGE_EQ_EMPTY] >> 691 `y IN (IMAGE deg t)` by rw[MIN_SET_LEM, Abbr`y`] >> 692 metis_tac[IN_IMAGE, in_preimage, poly_minimals_def, MEMBER_NOT_EMPTY]); 693 694(* Theorem: FiniteField r ==> !s. s <<= r ==> !x. x IN R ==> 695 (minimal x) IN (subfield_monics x) /\ 696 (degree x = MIN_SET (IMAGE deg (subfield_monics x))) *) 697(* Proof: 698 Let t = subfield_monics x, y = MIN_SET (IMAGE deg t), and p = minimal x. 699 Then p = CHOICE (preimage deg t y) by poly_minimal_def, poly_minimals_def 700 Now t <> {} by subfield_monics_of_element_nonempty 701 so IMAGE deg t <> {} by IMAGE_EQ_EMPTY, t <> {} 702 Thus y IN (IMAGE deg t) by MIN_SET_LEM, IMAGE deg t <> {} 703 Hence the result by preimage_choice_property 704*) 705val poly_minimal_property = store_thm( 706 "poly_minimal_property", 707 ``!(r s):'a field. FiniteField r /\ s <<= r ==> !x. x IN R ==> 708 (minimal x) IN (subfield_monics x) /\ 709 (degree x = MIN_SET (IMAGE deg (subfield_monics x)))``, 710 ntac 6 (stripDup[FiniteField_def]) >> 711 qabbrev_tac `t = subfield_monics x` >> 712 qabbrev_tac `y = MIN_SET (IMAGE deg t)` >> 713 qabbrev_tac `p = minimal x` >> 714 `p = CHOICE (preimage deg t y)` by rw[poly_minimal_def, poly_minimals_def, Abbr`p`, Abbr`t`, Abbr`y`] >> 715 `t <> {}` by rw[subfield_monics_of_element_nonempty, Abbr`t`] >> 716 `IMAGE deg t <> {}` by rw[IMAGE_EQ_EMPTY] >> 717 `y IN (IMAGE deg t)` by rw[MIN_SET_LEM, Abbr`y`] >> 718 rw[preimage_choice_property]); 719 720(* Theorem: FiniteField r ==> !s. s <<= r ==> 721 !x. x IN R ==> poly_monic s (minimal x) /\ 0 < degree x /\ root (minimal x) x *) 722(* Proof: 723 Let t = subfield_monics x, y = MIN_SET (IMAGE deg t), and p = minimal x. 724 Then p IN t /\ (deg p = y) by poly_minimal_property 725 and result follows by subfield_monics_of_element_member 726*) 727val poly_minimal_subfield_property = store_thm( 728 "poly_minimal_subfield_property", 729 ``!(r s):'a field. FiniteField r /\ s <<= r ==> 730 !x. x IN R ==> poly_monic s (minimal x) /\ 0 < degree x /\ root (minimal x) x``, 731 metis_tac[poly_minimal_property, subfield_monics_of_element_member]); 732 733(* Theorem: FiniteField r ==> !s. s <<= r ==> !x. x IN R ==> Poly s (minimal x) *) 734(* Proof: 735 Let t = subfield_monics x, y = MIN_SET (IMAGE deg t), and p = minimal x. 736 Since poly_monic s p by poly_minimal_subfield_property 737 or Poly s p by poly_monic_poly 738*) 739val poly_minimal_spoly = store_thm( 740 "poly_minimal_spoly", 741 ``!(r s):'a field. FiniteField r /\ s <<= r ==> !x. x IN R ==> Poly s (minimal x)``, 742 rw[poly_minimal_subfield_property]); 743 744(* Theorem: FiniteField r ==> !s. s <<= r ==> !x. x IN R ==> poly (minimal x) *) 745(* Proof: by poly_minimal_spoly, subfield_is_subring, subring_poly_poly *) 746val poly_minimal_poly = store_thm( 747 "poly_minimal_poly", 748 ``!(r s):'a field. FiniteField r /\ s <<= r ==> !x. x IN R ==> poly (minimal x)``, 749 metis_tac[poly_minimal_spoly, subfield_is_subring, subring_poly_poly]); 750 751(* Theorem: FiniteField r ==> !s. s <<= r ==> !x. x IN R ==> 0 < degree x *) 752(* Proof: by poly_minimal_subfield_property *) 753val poly_minimal_deg_pos = store_thm( 754 "poly_minimal_deg_pos", 755 ``!(r s):'a field. FiniteField r /\ s <<= r ==> !x. x IN R ==> 0 < degree x``, 756 rw[poly_minimal_subfield_property]); 757 758(* Theorem: FiniteField r /\ s <<= r ==> !x. x IN R ==> ~upoly (minimal x) *) 759(* Proof: 760 Since 0 < degree x by poly_minimal_deg_pos 761 but !p. upoly p ==> deg p = 0 by poly_field_unit_deg, Field r 762 so ~upoly (minimal x) 763*) 764val poly_minimal_not_unit = store_thm( 765 "poly_minimal_not_unit", 766 ``!(r s):'a field. FiniteField r /\ s <<= r ==> !x. x IN R ==> ~upoly (minimal x)``, 767 metis_tac[poly_minimal_deg_pos, poly_field_unit_deg, finite_field_is_field, NOT_ZERO_LT_ZERO]); 768 769(* Theorem: FiniteField r /\ s <<= r ==> !x. x IN R ==> (minimal x <> |1|) *) 770(* Proof: 771 Since 0 < degree x by poly_minimal_deg_pos 772 but deg |1| = 0 by poly_deg_one 773 so minimal x <> |1| 774*) 775val poly_minimal_ne_poly_one = store_thm( 776 "poly_minimal_ne_poly_one", 777 ``!(r s):'a field. FiniteField r /\ s <<= r ==> !x. x IN R ==> (minimal x <> |1|)``, 778 rpt (stripDup[FiniteField_def]) >> 779 `deg |1| = 0` by rw[] >> 780 metis_tac[poly_minimal_deg_pos, NOT_ZERO_LT_ZERO]); 781 782(* Theorem: FiniteField r /\ s <<= r ==> !x. x IN R ==> (minimal x <> |0|) *) 783(* Proof: 784 Since 0 < degree x by poly_minimal_deg_pos 785 but deg |0| = 0 by poly_deg_zero 786 so minimal x <> |0| 787*) 788val poly_minimal_ne_poly_zero = store_thm( 789 "poly_minimal_ne_poly_zero", 790 ``!(r s):'a field. FiniteField r /\ s <<= r ==> !x. x IN R ==> (minimal x <> |0|)``, 791 rpt (stripDup[FiniteField_def]) >> 792 `deg |0| = 0` by rw[] >> 793 metis_tac[poly_minimal_deg_pos, NOT_ZERO_LT_ZERO]); 794 795(* Theorem: FiniteField r ==> !s. s <<= r ==> !x. x IN R ==> root (minimal x) x *) 796(* Proof: by poly_minimal_subfield_property *) 797val poly_minimal_has_element_root = store_thm( 798 "poly_minimal_has_element_root", 799 ``!(r s):'a field. FiniteField r /\ s <<= r ==> !x. x IN R ==> root (minimal x) x``, 800 rw[poly_minimal_subfield_property]); 801 802(* Theorem: FiniteField r ==> !s. s <<= r ==> !x. x IN R ==> monic (minimal x) *) 803(* Proof: by poly_minimal_subfield_property, subfield_is_subring, subring_poly_monic *) 804val poly_minimal_monic = store_thm( 805 "poly_minimal_monic", 806 ``!(r s):'a field. FiniteField r /\ s <<= r ==> !x. x IN R ==> monic (minimal x)``, 807 metis_tac[poly_minimal_subfield_property, subfield_is_subring, subring_poly_monic]); 808 809(* Theorem: FiniteField r ==> !s. s <<= r ==> !x. x IN R ==> pmonic (minimal x) *) 810(* Proof: by poly_minimal_monic, poly_minimal_deg_pos, poly_monic_pmonic *) 811val poly_minimal_pmonic = store_thm( 812 "poly_minimal_pmonic", 813 ``!(r s):'a field. FiniteField r /\ s <<= r ==> !x. x IN R ==> pmonic (minimal x)``, 814 rw[poly_minimal_monic, poly_minimal_deg_pos, poly_monic_pmonic]); 815 816(* Theorem: FiniteField r ==> !s. s <<= r ==> !x. x IN R ==> 817 !p. Poly s p /\ root p x ==> (minimal x) pdivides p *) 818(* Proof: 819 Let q = minimal x. 820 Then poly_monic s q by poly_minimal_subfield_property 821 and Poly s q by poly_monic_poly 822 and 0 < deg q by poly_minimal_deg_pos 823 so 0 < Deg s q by subring_poly_deg 824 or Pmonic s q by poly_monic_pmonic 825 Hence ?u v. Poly s u /\ Poly s v /\ 826 (p = u * q + v) /\ deg v < deg q by subring_poly_division_eqn, 0 < deg q 827 Note poly p /\ poly q /\ poly u /\ poly v by subring_poly_poly 828 829 If v = |0|, 830 then p = u * q + |0| = u * q by poly_add_rzero 831 Hence q pdivides p by poly_divides_def 832 833 If v <> |0|, 834 Step 1: show that root z x. 835 then v = |1| * p - u * q by poly_sub_eq_add, poly_mult_lone 836 Since root p x by given 837 and root q x by poly_minimal_has_element_root 838 so root v x by poly_root_sub_linear 839 thus 0 < deg v by poly_nonzero_with_root_deg_pos 840 Let z be the monic version of v, 841 i.e. ?t z. Poly s t /\ poly_monic s z 842 and (deg z = deg v) /\ (z = t * v) by poly_monic_mult_by_factor, poly_unit_poly 843 Then root z x by poly_root_mult_comm 844 845 Step 2: show that z IN subfield_monics x. 846 With 0 < deg z = deg v, 847 z IN subfield_monics x by subfield_monics_of_element_member 848 849 Step 3, derive a contradiction. 850 Let m = subfield_monics x 851 Since z IN m, deg z IN IMAGE deg m by IN_IMAGE 852 or IMAGE deg m <> {} by MEMBER_NOT_EMPTY 853 Thus MIN_SET (IMAGE deg m) <= deg z by MIN_SET_LEM, IMAGE deg m <> {} 854 But deg q = MIN_SET (IMAGE deg m) by poly_minimal_property 855 and deg z = deg v < deg q by above 856 This contradicts with deg q <= deg z. 857*) 858val poly_minimal_divides_subfield_poly = store_thm( 859 "poly_minimal_divides_subfield_poly", 860 ``!(r s):'a field. FiniteField r /\ s <<= r ==> !x. x IN R ==> 861 !p. Poly s p /\ root p x ==> (minimal x) pdivides p``, 862 rpt (stripDup[FiniteField_def]) >> 863 `s <= r` by rw[subfield_is_subring] >> 864 qabbrev_tac `q = minimal x` >> 865 `poly_monic s q /\ Poly s q` by rw[poly_minimal_subfield_property, Abbr`q`] >> 866 `0 < deg q` by rw[poly_minimal_deg_pos, Abbr`q`] >> 867 `Pmonic s q` by metis_tac[poly_monic_pmonic, subring_poly_deg] >> 868 `?u v. Poly s u /\ Poly s v /\ (p = u * q + v) /\ deg v < deg q` by rw[subring_poly_division_eqn] >> 869 Cases_on `v = |0|` >- 870 metis_tac[poly_divides_def, subring_poly_poly, poly_mult_poly, poly_add_rzero] >> 871 `poly p /\ poly q /\ poly u /\ poly v` by metis_tac[subring_poly_poly] >> 872 `poly |1|` by rw[] >> 873 `v = |1| * p - u * q` by metis_tac[poly_sub_eq_add, poly_mult_lone, poly_mult_poly] >> 874 `root q x` by rw[poly_minimal_has_element_root, Abbr`q`] >> 875 `root v x` by rw[poly_root_sub_linear] >> 876 `0 < deg v` by metis_tac[poly_nonzero_with_root_deg_pos] >> 877 `poly_zero s = |0|` by rw[subring_poly_ids] >> 878 `?t z. Poly s t /\ poly_monic s z /\ 879 (poly_deg s z = poly_deg s v) /\ (z = poly_mult s t v)` by metis_tac[poly_monic_mult_by_factor, poly_unit_poly, field_is_ring] >> 880 `z = t * v` by metis_tac[subring_poly_mult, poly_monic_poly] >> 881 `poly t` by metis_tac[subring_poly_poly] >> 882 `root z x` by rw[poly_root_mult_comm] >> 883 `0 < deg z /\ deg z < deg q` by metis_tac[subring_poly_deg] >> 884 `z IN subfield_monics x` by rw[subfield_monics_of_element_member] >> 885 qabbrev_tac `m = subfield_monics x` >> 886 `deg z IN IMAGE deg m` by rw[] >> 887 `IMAGE deg m <> {}` by metis_tac[MEMBER_NOT_EMPTY] >> 888 `MIN_SET (IMAGE deg m) <= deg z` by rw[MIN_SET_LEM] >> 889 `deg q = MIN_SET (IMAGE deg m)` by rw[poly_minimal_property, Abbr`q`, Abbr`m`] >> 890 decide_tac); 891 892(* Theorem: FiniteField r /\ s <<= r ==> 893 !p x. Poly s p /\ x IN (roots p) ==> minimal x pdivides p *) 894(* Proof: by poly_minimal_divides_subfield_poly, poly_roots_member *) 895val poly_minimal_divides_subfield_poly_alt = store_thm( 896 "poly_minimal_divides_subfield_poly_alt", 897 ``!(r:'a field) s. FiniteField r /\ s <<= r ==> 898 !p x. Poly s p /\ x IN (roots p) ==> minimal x pdivides p``, 899 rw_tac std_ss[poly_minimal_divides_subfield_poly, poly_roots_member]); 900 901(* Theorem: FiniteField r /\ s <<= r ==> !x. x IN R ==> 902 !p. Poly s p ==> (root p x <=> (minimal x) pdivides p) *) 903(* Proof: 904 If part: root p x ==> (minimal x) pdivides p 905 True by poly_minimal_divides_subfield_poly. 906 Only-if part: (minimal x) pdivides p ==> root p x 907 Let q = minimal x. 908 Note root q x by poly_minimal_has_element_root 909 Now s <= r by subfield_is_subring 910 so poly p by subring_poly_poly 911 and poly q by poly_minimal_poly 912 ==> root p x by poly_divides_share_root 913*) 914val poly_minimal_divides_subfield_poly_iff = store_thm( 915 "poly_minimal_divides_subfield_poly_iff", 916 ``!(r s):'a field. FiniteField r /\ s <<= r ==> !x. x IN R ==> 917 !p. Poly s p ==> (root p x <=> (minimal x) pdivides p)``, 918 rpt (stripDup[FiniteField_def]) >> 919 qabbrev_tac `q = minimal x` >> 920 rw_tac std_ss[EQ_IMP_THM] >- 921 rw[poly_minimal_divides_subfield_poly, Abbr`q`] >> 922 `root q x` by rw[poly_minimal_has_element_root, Abbr`q`] >> 923 `s <= r` by rw[subfield_is_subring] >> 924 `poly p` by metis_tac[subring_poly_poly] >> 925 `poly q` by rw[poly_minimal_poly, Abbr`q`] >> 926 metis_tac[poly_divides_share_root]); 927 928(* This is a major milestone theorem. *) 929 930(* Theorem: FiniteField r /\ s <<= r ==> !x. x IN R ==> !p q. Poly s p /\ Poly s q ==> 931 ((eval p x = eval q x) <=> (p % (minimal x) = q % (minimal x))) *) 932(* Proof: 933 Let m = minimal x. 934 Then monic m by poly_minimal_monic 935 and 0 < deg m by poly_minimal_deg_pos 936 ==> pmonic m by poly_monic_pmonic 937 Let h = poly_sub s p q. 938 Note s <<= r ==> s <= r by subfield_is_subring 939 so h = p - q by subring_poly_sub 940 and Poly s h by poly_sub_poly 941 and poly p /\ poly q by subring_poly_poly 942 eval p x = eval q x 943 <=> eval p x - eval q x = #0 by field_sub_eq_zero 944 <=> eval (p - q) x = #0 by poly_eval_sub 945 <=> eval h x = #0 by above 946 <=> root h x by poly_root_def 947 <=> m pdivides h by poly_minimal_divides_subfield_poly_iff 948 <=> h % m = |0| by poly_divides_mod_zero, ulead m 949 <=> p % m = q % m by poly_mod_eq, ulead m 950*) 951val poly_minimal_eval_congruence = store_thm( 952 "poly_minimal_eval_congruence", 953 ``!(r:'a field) (s:'a field). FiniteField r /\ s <<= r ==> !x. x IN R ==> 954 !p q. Poly s p /\ Poly s q ==> ((eval p x = eval q x) <=> (p % (minimal x) = q % (minimal x)))``, 955 rpt (stripDup[FiniteField_def]) >> 956 qabbrev_tac `m = minimal x` >> 957 qabbrev_tac `h = poly_sub s p q` >> 958 `s <= r` by rw[subfield_is_subring] >> 959 `Poly s h /\ (h = p - q)` by rw[subring_poly_sub, Abbr`h`] >> 960 `monic m` by rw[poly_minimal_monic, Abbr`m`] >> 961 `pmonic m` by rw[poly_monic_pmonic, poly_minimal_deg_pos, Abbr`m`] >> 962 `poly p /\ poly q` by metis_tac[subring_poly_poly] >> 963 `(eval p x = eval q x) <=> (eval p x - eval q x = #0)` by rw[field_sub_eq_zero] >> 964 `_ = (eval h x = #0)` by rw[Abbr`h`] >> 965 `_ = root h x` by rw[poly_root_def] >> 966 `_ = (m pdivides h)` by rw[poly_minimal_divides_subfield_poly_iff, Abbr`m`] >> 967 `_ = (h % m = |0|)` by rw[poly_divides_mod_zero] >> 968 `_ = (p % m = q % m)` by rw[poly_mod_eq, Abbr`h`] >> 969 rw[]); 970 971(* Theorem: FiniteField r /\ s <<= r ==> !x. x IN R ==> (minimal x) pdivides (unity (forder x)) *) 972(* Proof: 973 Let ox = forder x. 974 If x = #0, 975 Then ox = 0 by field_order_zero 976 and unity 0 = |0| by poly_unity_0 977 Hence true by poly_divides_zero 978 If x <> #0, 979 Then x IN R+ by field_nonzero_eq 980 so x ** ox = #1 by field_order_property, x IN R+ 981 ==> root (unity ox) x by poly_unity_root_property 982 Also Poly s (unity ox) by poly_unity_spoly, subfield_is_subring 983 Hence (minimal x) pdivides (unity ox) by poly_minimal_divides_subfield_poly 984*) 985val poly_minimal_divides_unity_order = store_thm( 986 "poly_minimal_divides_unity_order", 987 ``!(r s):'a field. FiniteField r /\ s <<= r ==> !x. x IN R ==> (minimal x) pdivides (unity (forder x))``, 988 rpt (stripDup[FiniteField_def]) >> 989 qabbrev_tac `ox = forder x` >> 990 Cases_on `x = #0` >- 991 metis_tac[field_order_zero, poly_unity_0, poly_divides_zero, field_is_ring] >> 992 `x IN R+` by rw[field_nonzero_eq] >> 993 `x ** ox = #1` by rw[field_order_property, Abbr`ox`] >> 994 `root (unity ox) x` by rw[poly_unity_root_property] >> 995 `Poly s (unity ox)` by rw[poly_unity_spoly, subfield_is_subring] >> 996 rw[poly_minimal_divides_subfield_poly]); 997 998(* ------------------------------------------------------------------------- *) 999(* Minimal Polynomial is unique and irreducible *) 1000(* ------------------------------------------------------------------------- *) 1001 1002(* Theorem: FiniteField r ==> !s. s <<= r ==> !x. x IN R ==> SING (Minimals x) *) 1003(* Proof: 1004 Let t = Minimals x, p = minimal x. 1005 Then t <> {} by poly_minimals_nonempty 1006 and p IN t by poly_minimal_def, CHOICE_DEF, t <> {} 1007 Suppose q IN t. 1008 Then poly_monic s q /\ root q x by poly_minimals_member 1009 or Poly s q /\ root q x by poly_monic_poly 1010 Hence p pdivides q by poly_minimal_divides_subfield_poly 1011 But deg p = deg q = MIN_SET (IMAGE deg t) by poly_minimals_member 1012 and both p and q are monic by subring_poly_monic, subfield_is_subring 1013 so p = q by poly_monic_divides_eq_deg_eq 1014 or SING t by SING_ONE_ELEMENT 1015*) 1016val poly_minimals_sing = store_thm( 1017 "poly_minimals_sing", 1018 ``!(r s):'a field. FiniteField r /\ s <<= r ==> !x. x IN R ==> SING (Minimals x)``, 1019 rpt (stripDup[FiniteField_def]) >> 1020 qabbrev_tac `t = Minimals x` >> 1021 qabbrev_tac `p = minimal x` >> 1022 `t <> {}` by rw[poly_minimals_nonempty, Abbr`t`] >> 1023 `p IN t` by rw[poly_minimal_def, CHOICE_DEF, Abbr`p`, Abbr`t`] >> 1024 `!q. q IN t ==> (p = q)` suffices_by metis_tac[SING_ONE_ELEMENT] >> 1025 rpt strip_tac >> 1026 `poly_monic s q /\ root q x` by metis_tac[poly_minimals_member] >> 1027 `Poly s q` by rw[poly_monic_poly] >> 1028 `p pdivides q` by rw[poly_minimal_divides_subfield_poly, Abbr`p`] >> 1029 `deg p = deg q` by metis_tac[poly_minimals_member] >> 1030 `monic p /\ monic q` by metis_tac[poly_minimals_member, subfield_is_subring, subring_poly_monic] >> 1031 metis_tac[poly_monic_divides_eq_deg_eq]); 1032 1033(* Theorem: FiniteField r ==> !s. s <<= r ==> (minimal #0 = X) *) 1034(* Proof: 1035 Let p = X + |c| be a monic degree 1 polynomial. 1036 In order that #0 is a root of p, eval (X + |c|) #0 = #0 1037 or #0 + c = #0 ==> c = #0. 1038 Hence p = X is the only choice. 1039 and with deg p = 1, it must be the minimal. 1040 1041 Step 1: show X is a candidate. 1042 Note lead X = #1 by poly_lead_X 1043 and deg X = 1, or 0 < deg X by poly_deg_X 1044 also root X #0 by poly_root_def, poly_eval_cons 1045 Since (s.sum.id = #0) /\ (s.prod.id = #1) by subfield_ids 1046 so #0 IN B and #1 IN B by field_zero_element, field_one_element 1047 Thus Poly s X by Poly_def, zero_poly_def 1048 and poly_lead s X = s.prod.id by subring_poly_lead, subfield_is_subring 1049 so poly_monic s X by poly_monic_def 1050 1051 Let t = Minimals #0, 1052 Then X IN t by poly_minimals_has_monoimal_condition, #0 IN R 1053 1054 Step 2: apply property of SING. 1055 Since X IN t, t <> {} by MEMBER_NOT_EMPTY 1056 and poly_minimal r s #0 IN t by poly_minimal_def, CHOICE_DEF, t <> {} 1057 But SING t by poly_minimals_sing 1058 Hence poly_minimal r s #0 = X by SING_ONE_ELEMENT 1059*) 1060val poly_minimal_zero = store_thm( 1061 "poly_minimal_zero", 1062 ``!(r s):'a field. FiniteField r /\ s <<= r ==> (minimal #0 = X)``, 1063 rpt (stripDup[FiniteField_def]) >> 1064 `(lead X = #1) /\ (deg X = 1)` by rw[] >> 1065 `root X #0` by rw[poly_root_def] >> 1066 `0 < deg X` by decide_tac >> 1067 `#0 IN R /\ #0 IN B /\ #1 IN B /\ (s.sum.id = #0) /\ (s.prod.id = #1)` by metis_tac[subfield_ids, field_zero_element, field_one_element] >> 1068 `Poly s X` by rw[] >> 1069 `poly_lead s X = s.prod.id` by rw[subring_poly_lead, subfield_is_subring] >> 1070 `poly_monic s X` by metis_tac[poly_monic_def] >> 1071 qabbrev_tac `t = poly_minimals r s #0` >> 1072 `X IN t` by metis_tac[poly_minimals_has_monoimal_condition, Abbr`t`] >> 1073 `t <> {}` by metis_tac[MEMBER_NOT_EMPTY] >> 1074 `minimal #0 IN t` by rw[poly_minimal_def, CHOICE_DEF, Abbr`t`] >> 1075 metis_tac[poly_minimals_sing, SING_ONE_ELEMENT]); 1076 1077(* Theorem: FiniteField r /\ s <<= r ==> (minimal #1 = X - |1|) *) 1078(* Proof: 1079 Let p = X + |c| be a monic degree 1 polynomial. 1080 In order that #1 is a root of p, eval (X + |c|) #1 = #1 + c 1081 or #1 + c = #0 ==> c = - #1. 1082 Hence p = X - |1| is the only choice. 1083 and with deg p = 1, it must be the minimal. 1084 1085 Let p = X - |1|, t = Minimals #1. 1086 Note p = unity 1 by poly_unity_1 1087 Step 1: show p is a candidate. 1088 Since deg p = 1 by poly_unity_deg 1089 and poly_monic s p by poly_unity_monic, subring_poly_unity, subfield_is_subring 1090 and root p #1 by poly_unity_root_has_one 1091 Thus p IN t by poly_minimals_has_monoimal_condition 1092 1093 Step 2: apply property of SING. 1094 Since p IN t, t <> {} by MEMBER_NOT_EMPTY 1095 and minimal #1 IN t by poly_minimal_def, CHOICE_DEF, t <> {} 1096 But SING t by poly_minimals_sing 1097 Hence minimal #1 = p by SING_ONE_ELEMENT 1098*) 1099val poly_minimal_one = store_thm( 1100 "poly_minimal_one", 1101 ``!(r s):'a ring. FiniteField r /\ s <<= r ==> (minimal #1 = X - |1|)``, 1102 rpt (stripDup[FiniteField_def]) >> 1103 qabbrev_tac `p = X - |1|` >> 1104 `p = unity 1` by rw[poly_unity_1, Abbr`p`] >> 1105 `deg p = 1` by rw[poly_unity_deg] >> 1106 `poly_monic s (Unity s 1)` by rw[poly_unity_monic] >> 1107 `poly_monic s p` by metis_tac[subring_poly_unity, subfield_is_subring] >> 1108 `root p #1` by rw[poly_unity_root_has_one] >> 1109 qabbrev_tac `t = Minimals #1` >> 1110 `p IN t` by rw[poly_minimals_has_monoimal_condition, Abbr`t`] >> 1111 `t <> {}` by metis_tac[MEMBER_NOT_EMPTY] >> 1112 `minimal #1 IN t` by rw[poly_minimal_def, CHOICE_DEF, Abbr`t`] >> 1113 `#1 IN R` by rw[] >> 1114 `SING t` by rw[poly_minimals_sing, Abbr`t`] >> 1115 metis_tac[SING_DEF, IN_SING]); 1116 1117(* Theorem: FiniteField r /\ s <<= r ==> !x. x IN R ==> ((minimal x = X) <=> (x = #0)) *) 1118(* Proof: 1119 If part: minimal x = X ==> x = #0 1120 Since root (minimal x) x by poly_minimal_has_element_root 1121 or root X x by minimal x = X 1122 <=> eval X x = #0 by poly_root_def 1123 <=> x = #0 by poly_eval_X 1124 Only-if part: x = #0 ==> minimal x = X, true by poly_minimal_zero 1125*) 1126val poly_minimal_eq_X = store_thm( 1127 "poly_minimal_eq_X", 1128 ``!(r s):'a field. FiniteField r /\ s <<= r ==> !x. x IN R ==> ((minimal x = X) <=> (x = #0))``, 1129 metis_tac[poly_minimal_has_element_root, poly_minimal_zero, poly_root_def, poly_eval_X, field_is_ring]); 1130 1131(* Theorem: FiniteField r ==> !s. s <<= r ==> !x. x IN R ==> IPoly s (minimal x *) 1132(* Proof: 1133 Let p = minimal x. 1134 Then poly_monic s p /\ 0 < deg p /\ root p x by poly_minimal_subfield_property 1135 or 0 < poly_deg s p by subring_poly_deg 1136 By contradiction, suppose ~IPoly s p. 1137 Then ?u v. poly_monic s u /\ poly_monic s v /\ (p = poly_mult s u v) /\ 1138 0 < poly_deg s u /\ 0 < poly_deg s v /\ poly_deg s u < poly_deg s p /\ poly_deg s v < poly_deg s p 1139 by poly_monic_reducible_factors 1140 or p = u * v by subring_poly_mult 1141 and 0 < deg u /\ deg u < deg p by subring_poly_deg, poly_monic_poly 1142 and 0 < deg v /\ deg v < deg p by subring_poly_deg, poly_monic_poly 1143 Let t = subfield_monics x 1144 then t <> {} by subfield_monics_of_element_nonempty 1145 and IMAGE deg t <> {} by IMAGE_EQ_EMPTY 1146 with deg p = MIN_SET (IMAGE deg t) by poly_minimal_property 1147 1148 Since root p x by above, or poly_minimal_has_element_root 1149 so root u x or root v x by poly_root_field_mult 1150 If root u x, 1151 Then u IN t by subfield_monics_of_element_member 1152 so deg u IN (IMAGE deg t) by IN_IMAGE 1153 or MIN_SET (IMAGE deg t) <= deg u by MIN_SET_LEM 1154 This contradicts deg u < deg p = MIN_SET (IMAGE deg t) 1155 If root v x, 1156 Then v IN t by subfield_monics_of_element_member 1157 so deg v IN (IMAGE deg t) by IN_IMAGE 1158 or MIN_SET (IMAGE deg t) <= deg v by MIN_SET_LEM 1159 This contradicts deg v < deg p = MIN_SET (IMAGE deg t) 1160*) 1161val poly_minimal_subfield_irreducible = store_thm( 1162 "poly_minimal_subfield_irreducible", 1163 ``!(r s):'a field. FiniteField r /\ s <<= r ==> !x. x IN R ==> IPoly s (minimal x)``, 1164 rpt (stripDup[FiniteField_def]) >> 1165 `s <= r` by rw[subfield_is_subring] >> 1166 qabbrev_tac `p = minimal x` >> 1167 `poly_monic s p /\ 0 < deg p /\ root p x` by rw[poly_minimal_subfield_property, Abbr`p`] >> 1168 `0 < poly_deg s p` by metis_tac[subring_poly_deg] >> 1169 spose_not_then strip_assume_tac >> 1170 `?u v. poly_monic s u /\ poly_monic s v /\ (p = poly_mult s u v) /\ 1171 0 < poly_deg s u /\ 0 < poly_deg s v /\ poly_deg s u < poly_deg s p /\ poly_deg s v < poly_deg s p` by rw[poly_monic_reducible_factors] >> 1172 `Poly s p /\ Poly s u /\ Poly s v` by rw[] >> 1173 `poly p /\ poly u /\ poly v` by metis_tac[subring_poly_poly] >> 1174 `(p = u * v) /\ 0 < deg u /\ 0 < deg v /\ deg u < deg p /\ deg v < deg p` by metis_tac[subring_poly_mult, subring_poly_deg] >> 1175 qabbrev_tac `t = subfield_monics x` >> 1176 `t <> {}` by rw[subfield_monics_of_element_nonempty, Abbr`t`] >> 1177 `IMAGE deg t <> {}` by rw[] >> 1178 `deg p = MIN_SET (IMAGE deg t)` by rw[poly_minimal_property, Abbr`t`, Abbr`p`] >> 1179 `root u x \/ root v x` by metis_tac[poly_root_field_mult] >| [ 1180 `u IN t` by rw[subfield_monics_of_element_member, Abbr`t`] >> 1181 `MIN_SET (IMAGE deg t) <= deg u` by rw[MIN_SET_LEM] >> 1182 decide_tac, 1183 `v IN t` by rw[subfield_monics_of_element_member, Abbr`t`] >> 1184 `MIN_SET (IMAGE deg t) <= deg v` by rw[MIN_SET_LEM] >> 1185 decide_tac 1186 ]); 1187 1188(* This is a milestone theorem. *) 1189 1190(* ------------------------------------------------------------------------- *) 1191(* Minimal Polynomial of Prime Field *) 1192(* ------------------------------------------------------------------------- *) 1193 1194(* 1195The following prime field theorems can be proved by subfield/subring. 1196Proofs below to be revised. 1197*) 1198 1199(* Theorem: FiniteField r ==> !p n. p IN sticks (PF r) n ==> weak p *) 1200(* Proof: 1201 Since Field r by FiniteField_def 1202 and Field (PF r) by prime_field_field 1203 and subfield (PF r) r by prime_field_subfield 1204 Now Weak (PF r) p by stick_is_weak 1205 hence weak p by subfield_poly_weak_is_weak 1206*) 1207val prime_field_stick_is_weak = store_thm( 1208 "prime_field_stick_is_weak", 1209 ``!r:'a field. FiniteField r ==> !p n. p IN sticks (PF r) n ==> weak p``, 1210 rpt (stripDup[FiniteField_def]) >> 1211 `Field (PF r)` by rw[prime_field_field] >> 1212 `subfield (PF r) r` by rw[prime_field_subfield] >> 1213 metis_tac[stick_is_weak, subfield_poly_weak_is_weak]); 1214 1215(* Theorem: FiniteField r ==> !p n. p IN sticks (PF r) (SUC n) ==> 1216 !x. x IN R ==> (p <o> (ebasis x n) = eval p x) *) 1217(* Proof: 1218 By induction on n. 1219 Base case: !p. p IN sticks (PF r) (SUC 0) ==> 1220 !x. x IN R ==> (p <o> ebasis x 0 = eval p x) 1221 p IN sticks (PF r) (SUC 0) 1222 ==> p IN sticks (PF r) 1 by ONE 1223 ==> ?c. c IN Fp /\ (p = [c]) by sticks_1_member 1224 Note c IN R by prime_field_element 1225 Also ebasis x 0 = [#1] by element_powers_basis_0 1226 VectorSum r.sum (MAP2 $* [c] [#1]) 1227 = VectorSum r.sum [c * #1] by MAP2 1228 = VectorSum r.sum [c] by ring_mult_rone 1229 = c + (VectorSum r.sum []) by vsum_cons 1230 = c + #0 by vsum_nil 1231 = c by ring_add_rzero 1232 = eval [c] x by poly_eval_const 1233 Step case: !p. p IN sticks (PF r) (SUC (SUC n)) ==> 1234 !x. x IN R ==> (p <o> ebasis x (SUC n) = eval p x) 1235 p IN sticks (PF r) (SUC (SUC n)) 1236 ==> ?h t. h IN Fp /\ t IN sticks (PF r) (SUC n) /\ (p = SNOC h t) 1237 by stick_snoc 1238 Note LENGTH t = SUC n by stick_length 1239 Also ebasis x (SUC n) = SNOC (x ** (SUC n)) (ebasis x n) by element_powers_basis_suc 1240 and h IN R by prime_field_element 1241 and weak t by prime_field_stick_is_weak 1242 and eval t x IN R by weak_eval_element 1243 p <o> (ebasis x (SUC n))) 1244 = (SNOC h t) <o> (SNOC (x ** (SUC n)) (ebasis x n)) by above 1245 = h * (x ** SUC n) + t <o> (ebasis x n) by vsum_stick_snoc 1246 = h * (x ** SUC n) + eval t x by induction hypothesis 1247 = eval t x + h * x ** LENGTH t by ring_add_comm 1248 = eval (SNOC h t) x by weak_eval_snoc 1249 = eval p x by p = SNOC h t 1250*) 1251val vsum_element_powers_basis_eq_eval = store_thm( 1252 "vsum_element_powers_basis_eq_eval", 1253 ``!r:'a field. FiniteField r ==> !p n. p IN sticks (PF r) (SUC n) ==> 1254 !x. x IN R ==> (p <o> (ebasis x n) = eval p x)``, 1255 ntac 2 (stripDup[FiniteField_def]) >> 1256 Induct_on `n` >| [ 1257 rw[] >> 1258 `?c. c IN Fp /\ (p = [c])` by rw[GSYM sticks_1_member] >> 1259 `c IN R` by rw[prime_field_element] >> 1260 `ebasis x 0 = [#1]` by rw[element_powers_basis_0] >> 1261 rw[vsum_cons, vsum_nil], 1262 rpt strip_tac >> 1263 `?h t. h IN Fp /\ t IN sticks (PF r) (SUC n) /\ (p = SNOC h t)` by rw[GSYM stick_snoc] >> 1264 `ebasis x (SUC n) = SNOC (x ** (SUC n)) (ebasis x n)` by rw_tac std_ss[element_powers_basis_suc] >> 1265 `VSpace (PF r) r.sum $*` by rw[finite_field_is_vspace] >> 1266 `basis r.sum (ebasis x n)` by rw[element_powers_basis_is_basis] >> 1267 `LENGTH (ebasis x n) = SUC n` by rw[element_powers_basis_length] >> 1268 `x ** SUC n IN R /\ (R = r.sum.carrier)` by rw[] >> 1269 `h IN R` by rw[prime_field_element] >> 1270 `weak t` by metis_tac[prime_field_stick_is_weak] >> 1271 `p <o> (ebasis x (SUC n)) = h * (x ** SUC n) + eval t x` by metis_tac[vsum_stick_snoc] >> 1272 `_ = h * x ** LENGTH t + eval t x` by metis_tac[stick_length] >> 1273 `_ = eval t x + h * x ** LENGTH t` by rw[ring_add_comm] >> 1274 `_ = eval p x` by rw[weak_eval_snoc] >> 1275 rw[] 1276 ]); 1277 1278(* Theorem: FiniteField r ==> !x. x IN R ==> ?p. pfpoly p /\ 0 < deg p /\ root p x *) 1279(* Proof: 1280 Let n = dim (PF r) r.sum $*, b = ebasis x n. 1281 Then ~LinearIndepBasis (PF r) r.sum $* b by element_powers_basis_dim_dep 1282 Note basis r.sum b by element_powers_basis_is_basis 1283 and LENGTH b = SUC n by element_powers_basis_length 1284 and (PF r).sum.id = #0 by PF_property 1285 Hence by LinearIndepBasis_def, 1286 ?q. q IN sticks (PF r) (SUC n) /\ 1287 ~(q <o> b) = #0) <=> !k. k < SUC n ==> (EL k q = #0)) [1] 1288 1289 Note VSpace (PF r) r.sum $* by finite_field_is_vspace 1290 and !k. k < SUC n ==> (EL k q = #0)) ==> (q <o> b) = #0) by vspace_stick_zero 1291 Thus ?k. k < SUC n /\ (EL k p <> #0) /\ (q <o> b) = #0) by [1] 1292 Now Weak (PF r) q by stick_is_weak 1293 and LENGTH q = SUC n by stick_length 1294 so ~pfzerop q by zero_poly_element, EL k q <> #0 1295 Let p = pfchop q 1296 Then pfpoly p by poly_chop_weak_poly 1297 and ~pfzerop p by zero_poly_eq_zero_poly_chop 1298 thus p <> PolyRing (PF r)).sum.id by zero_poly_eq_poly_zero 1299 or p <> |0| by poly_prime_field_ids 1300 Also eval p x = eval (pfchop q) x 1301 = eval (chop q) x by poly_prime_field_chop 1302 = eval q x by poly_eval_chop 1303 = q <o> b by vsum_element_powers_basis_eq_eval 1304 = #0 by above 1305 Hence root p x by poly_root_def 1306 with 0 < deg p by poly_nonzero_with_root_deg_pos 1307*) 1308val poly_prime_field_with_root_exists = store_thm( 1309 "poly_prime_field_with_root_exists", 1310 ``!r:'a field. FiniteField r ==> !x. x IN R ==> ?p. pfpoly p /\ 0 < deg p /\ root p x``, 1311 rpt (stripDup[FiniteField_def]) >> 1312 qabbrev_tac `n = dim (PF r) r.sum $*` >> 1313 qabbrev_tac `b = ebasis x n` >> 1314 `~LinearIndepBasis (PF r) r.sum $* b` by rw[element_powers_basis_dim_dep, Abbr`n`, Abbr`b`] >> 1315 `basis r.sum b` by rw[element_powers_basis_is_basis, Abbr`b`] >> 1316 `LENGTH b = SUC n` by rw[element_powers_basis_length, Abbr`b`] >> 1317 `(PF r).sum.id = #0` by rw[PF_property] >> 1318 `?q. q IN sticks (PF r) (SUC n) /\ 1319 ~((q <o> b = #0) <=> !k. k < SUC n ==> (EL k q = #0))` by metis_tac[LinearIndepBasis_def] >> 1320 `VSpace (PF r) r.sum $*` by rw[finite_field_is_vspace] >> 1321 `?k. k < SUC n /\ (EL k q <> #0) /\ (q <o> b = #0)` by metis_tac[vspace_stick_zero] >> 1322 `Weak (PF r) q` by metis_tac[stick_is_weak] >> 1323 qexists_tac `pfchop q` >> 1324 `pfpoly (pfchop q)` by metis_tac[poly_chop_weak_poly] >> 1325 `eval q x = #0` by metis_tac[vsum_element_powers_basis_eq_eval] >> 1326 `root (chop q) x` by rw[poly_root_def] >> 1327 `root (pfchop q) x` by rw[poly_prime_field_chop] >> 1328 `~pfzerop q` by metis_tac[zero_poly_element, stick_length] >> 1329 `~pfzerop (pfchop q)` by metis_tac[zero_poly_eq_zero_poly_chop] >> 1330 `(pfchop q) <> |0|` by metis_tac[zero_poly_eq_poly_zero, poly_prime_field_ids] >> 1331 `poly (pfchop q)` by rw[poly_prime_field_element_poly] >> 1332 `0 < deg (pfchop q)` by metis_tac[poly_nonzero_with_root_deg_pos, field_is_ring] >> 1333 rw[]); 1334 1335(* overload on monic in (PF r) poly *) 1336val _ = overload_on("pfmonic", ``poly_monic (PF r)``); 1337(* overload on ipoly in (PF r) poly *) 1338val _ = overload_on("pfipoly", ``irreducible (PolyRing (PF r))``); 1339 1340(* Theorem: FiniteField r ==> !x. x IN R ==> ?p. pfmonic p /\ 0 < deg p /\ root p x *) 1341(* Proof: 1342 Since FiniteField r 1343 ==> ?q. pfpoly q /\ 0 < deg q /\ root q x by poly_prime_field_with_root_exists 1344 Note (PolyRing (PF r)).sum.id = |0| by poly_prime_field_ids 1345 and Field (PF r) by prime_field_field 1346 Hence ?u p. pfpoly u /\ pfmonic p /\ (pfdeg p = pfdeg q) /\ (p = pfmult u q) by poly_monic_mult_by_factor, poly_unit_poly 1347 with 0 < deg q = pfdeg q = pfdeg p = deg p by poly_prime_field_deg 1348 Since pfpoly p by poly_monic_poly 1349 Thus poly u /\ poly p /\ poly q /\ by poly_prime_field_element_poly 1350 (p = u * q) by poly_prime_field_mult 1351 eval p x 1352 = (eval u x) * (eval q x) by poly_eval_mult 1353 = (eval u x) * #0 by poly_root_def 1354 = #0 by poly_eval_element, field_mult_rzero 1355 Hence root p x by poly_root_def 1356*) 1357val poly_prime_field_monic_with_root_exists = store_thm( 1358 "poly_prime_field_monic_with_root_exists", 1359 ``!r:'a field. FiniteField r ==> !x. x IN R ==> ?p. pfmonic p /\ 0 < deg p /\ root p x``, 1360 rpt (stripDup[FiniteField_def]) >> 1361 `?q. pfpoly q /\ 0 < deg q /\ root q x` by rw_tac std_ss[poly_prime_field_with_root_exists] >> 1362 `(PolyRing (PF r)).sum.id = |0|` by rw[poly_prime_field_ids] >> 1363 `Field (PF r)` by rw[prime_field_field] >> 1364 `q <> |0|` by rw[poly_deg_pos_nonzero] >> 1365 `?u p. pfpoly u /\ pfmonic p /\ (pfdeg p = pfdeg q) /\ (p = pfmult u q)` by metis_tac[poly_monic_mult_by_factor, poly_unit_poly, field_is_ring] >> 1366 `0 < deg p` by metis_tac[poly_prime_field_deg] >> 1367 `Ring r /\ pfpoly p` by rw[] >> 1368 `poly u /\ poly p /\ poly q /\ (p = u * q)` by rw[poly_prime_field_element_poly, poly_prime_field_mult] >> 1369 `eval p x = (eval u x) * (eval q x)` by rw_tac std_ss[poly_eval_mult] >> 1370 `_ = (eval u x) * #0` by metis_tac[poly_root_def] >> 1371 `_ = #0` by rw[] >> 1372 metis_tac[poly_root_def]); 1373 1374 1375(* ------------------------------------------------------------------------- *) 1376(* Ideals of Polynomial Ring *) 1377(* ------------------------------------------------------------------------- *) 1378 1379(* 1380> ringIdealTheory.ideal_has_principal_ideal; 1381val it = |- !r i. Ring r /\ i << r ==> !p. p IN R ==> (p IN i.carrier <=> <p> << i): thm 1382> ringIdealTheory.ideal_has_principal_ideal |> ISPEC ``(PolyRing r)``; 1383val it = |- !i. Ring (PolyRing r) /\ i << PolyRing r ==> 1384 !p. p IN (PolyRing r).carrier ==> (p IN i.carrier <=> principal_ideal (PolyRing r) p << i): thm 1385*) 1386 1387(* overload on principal ideal in (PolyRing r) *) 1388val _ = overload_on("pfppideal", ``principal_ideal (PolyRing r)``); 1389 1390(* Theorem: Ring r ==> !p. poly p ==> ((pfppideal p = pfppideal |0|) <=> (p = |0|)) *) 1391(* Proof: 1392 If part: pfppideal p = pfppideal |0| ==> p = |0| 1393 Since Ring (PolyRing r) by poly_ring_ring 1394 and p IN (PolyRing r).carrier by poly_ring_property 1395 thus p IN (pfppideal p).carrier by principal_ideal_has_element 1396 Also (pfppideal p).carrier 1397 = (pfppideal |0|).carrier by principal_ideal_ideal, ideal_eq_ideal 1398 = {|0|} by zero_ideal_sing 1399 Hence p = |0| by IN_SING 1400 Only-if part: p = |0| ==> pfppideal p = pfppideal |0| 1401 This is trivial. 1402*) 1403val poly_ring_zero_ideal = store_thm( 1404 "poly_ring_zero_ideal", 1405 ``!r:'a ring. Ring r ==> !p. poly p ==> ((pfppideal p = pfppideal |0|) <=> (p = |0|))``, 1406 rw_tac std_ss[EQ_IMP_THM] >> 1407 `poly |0|` by rw[] >> 1408 `Ring (PolyRing r)` by rw[poly_ring_ring] >> 1409 `p IN (pfppideal p).carrier` by metis_tac[principal_ideal_has_element, poly_ring_property] >> 1410 `(pfppideal p).carrier = (pfppideal |0|).carrier` by rw[principal_ideal_ideal, ideal_eq_ideal] >> 1411 `_ = {|0|}` by rw[zero_ideal_sing] >> 1412 metis_tac[IN_SING]); 1413 1414(* Theorem: Field r ==> !i. i << (PolyRing r) /\ i <> pfppideal |0| ==> ?p. monic p /\ (i = pfppideal p) *) 1415(* Proof: 1416 Since Ring (PolyRing r) by poly_ring_ring, Ring r` 1417 and PrincipalIdealRing (PolyRing r) by poly_ring_principal_ideal_ring, Field r 1418 so ?q. poly q /\ (i = pfppideal q) by PrincipalIdealRing_def, poly_ring_property 1419 and q <> |0| by poly_ring_zero_ideal 1420 thus ?u p. upoly u /\ 1421 monic p /\ (deg p = deg q) /\ (q = u * p) by poly_monic_mult_factor 1422 and poly u by poly_unit_poly 1423 and poly p by poly_monic_def 1424 Now q = p * u by poly_mult_comm 1425 Hence i = pfppideal p by principal_ideal_eq_principal_ideal, Ring (PolyRing r) 1426*) 1427val poly_ring_ideal_gen_monic = store_thm( 1428 "poly_ring_ideal_gen_monic", 1429 ``!r:'a field. Field r ==> !i. i << (PolyRing r) /\ i <> pfppideal |0| ==> 1430 ?p. monic p /\ (i = pfppideal p)``, 1431 rpt strip_tac >> 1432 `Ring (PolyRing r)` by rw[poly_ring_ring] >> 1433 `PrincipalIdealRing (PolyRing r)` by rw[poly_ring_principal_ideal_ring] >> 1434 `?q. poly q /\ (i = pfppideal q)` by metis_tac[PrincipalIdealRing_def, poly_ring_property] >> 1435 `q <> |0|` by metis_tac[poly_ring_zero_ideal] >> 1436 `?u p. upoly u /\ monic p /\ (deg p = deg q) /\ (q = u * p)` by rw[poly_monic_mult_factor] >> 1437 `poly p /\ poly u` by rw[poly_unit_poly] >> 1438 `q = p * u` by rw[poly_mult_comm] >> 1439 metis_tac[principal_ideal_eq_principal_ideal, poly_ring_property]); 1440 1441(* Theorem: Field r ==> !p q. poly p /\ poly q ==> 1442 ((pfppideal p = pfppideal q) <=> ?u. poly u /\ upoly u /\ (p = u * q)) *) 1443(* Proof: 1444 Note Ring r by field_is_ring 1445 and Ring (PolyRing r) by poly_ring_ring 1446 If part: pfppideal p = pfppideal q ==> ?u. poly u /\ upoly u /\ (p = u * q) 1447 If p = |0|, 1448 then q = |0| by poly_ring_zero_ideal 1449 Take u = |1|, 1450 then poly |1| by poly_one_poly 1451 and upoly |1| by poly_field_unit_one 1452 and |0| = |1| * |0| by poly_mult_lone 1453 If p <> |0|, 1454 then p IN (pfppideal q).carrier by principal_ideal_has_element 1455 and q IN (pfppideal p).carrier by principal_ideal_has_element 1456 so ?u. poly u /\ (p = q * u) by principal_ideal_element 1457 and ?v. poly v /\ (q = p * v) by principal_ideal_element 1458 Now p * |1| 1459 = p by poly_mult_rone 1460 = q * u by above 1461 = (p * v) * u by above 1462 = p * (v * u) by poly_mult_assoc 1463 Therefore, 1464 v * u = |1| by poly_mult_lcancel, p <> |0| 1465 or u * v = |1| by poly_mult_comm 1466 thus upoly u by poly_ring_units 1467 and p = q * u = u * q by poly_mult_comm 1468 Only-if part: ?u. poly u /\ upoly u /\ (p = u * q) ==> pfppideal p = pfppideal q 1469 or to show: pfppideal (u * q) = pfppideal q 1470 Since p = u * q = q * u by poly_mult_comm 1471 Hence pfppideal p = pfppideal q by principal_ideal_eq_principal_ideal 1472*) 1473val poly_field_principal_ideal_equal = store_thm( 1474 "poly_field_principal_ideal_equal", 1475 ``!r:'a field. Field r ==> !p q. poly p /\ poly q ==> 1476 ((pfppideal p = pfppideal q) <=> ?u. poly u /\ upoly u /\ (p = u * q))``, 1477 rpt strip_tac >> 1478 `Ring r` by rw[] >> 1479 `Ring (PolyRing r)` by rw[poly_ring_ring] >> 1480 `!p. poly p <=> p IN (PolyRing r).carrier` by rw[poly_ring_element] >> 1481 rw[EQ_IMP_THM] >| [ 1482 Cases_on `p = |0|` >| [ 1483 `q = |0|` by rw[GSYM poly_ring_zero_ideal] >> 1484 qexists_tac `|1|` >> 1485 rw[poly_field_unit_one], 1486 `p IN (pfppideal q).carrier` by metis_tac[principal_ideal_has_element] >> 1487 `q IN (pfppideal p).carrier` by metis_tac[principal_ideal_has_element] >> 1488 `?u. poly u /\ (p = q * u)` by metis_tac[principal_ideal_element] >> 1489 `?v. poly v /\ (q = p * v)` by metis_tac[principal_ideal_element] >> 1490 `p * |1| = p` by rw[] >> 1491 `_ = p * v * u` by rw[] >> 1492 `_ = p * (v * u)` by rw[poly_mult_assoc] >> 1493 `v * u = |1|` by prove_tac[poly_mult_lcancel, poly_one_poly, poly_mult_poly] >> 1494 metis_tac[poly_ring_units, poly_mult_comm] 1495 ], 1496 metis_tac[principal_ideal_eq_principal_ideal, poly_mult_comm] 1497 ]); 1498 1499(* Theorem: Field r ==> !p q. monic p /\ monic q /\ (pfppideal p = pfppideal q) ==> (p = q) *) 1500(* Proof: 1501 Since ?u. poly u /\ upoly u /\ (p = u * q) by poly_field_principal_ideal_equal 1502 and upoly u 1503 ==> u <> |0| /\ (deg u = 0) by poly_field_units 1504 ==> ?c. c IN R /\ c <> #0 /\ (u = [c]) by poly_deg_eq_0 1505 In Field r, since p = u * q, 1506 lead p = lead u * lead q by poly_lead_mult 1507 or #1 = c * #1 by poly_monic_lead, poly_lead_const 1508 or #1 = c by field_mult_rone 1509 thus u = [#1] = |1| by poly_one, field_one_ne_zero 1510 Hence p = u * q = |1| * q = q by poly_mult_lone, poly_monic_poly 1511*) 1512val poly_ring_ideal_monic_gen_unique = store_thm( 1513 "poly_ring_ideal_monic_gen_unique", 1514 ``!r:'a field. Field r ==> !p q. monic p /\ monic q /\ (pfppideal p = pfppideal q) ==> (p = q)``, 1515 rpt strip_tac >> 1516 `?u. poly u /\ upoly u /\ (p = u * q)` by rw[GSYM poly_field_principal_ideal_equal] >> 1517 `u <> |0| /\ (deg u = 0)` by metis_tac[poly_field_units] >> 1518 `?c. c IN R /\ c <> #0 /\ (u = [c])` by rw[GSYM poly_deg_eq_0] >> 1519 `lead p = lead u * lead q` by rw[poly_lead_mult] >> 1520 `#1 = c * #1` by metis_tac[poly_monic_lead, poly_lead_const] >> 1521 `c = #1` by metis_tac[field_mult_rone] >> 1522 `u = |1|` by metis_tac[poly_one, field_one_ne_zero] >> 1523 rw[]); 1524 1525(* ------------------------------------------------------------------------- *) 1526(* The Ideal of Polynomials sharing a root. *) 1527(* ------------------------------------------------------------------------- *) 1528 1529(* Make an ideal from a set *) 1530val set_to_ideal_def = Define ` 1531 set_to_ideal (r:'a ring) (s:'a -> bool) = 1532 <| carrier := s; 1533 sum := <| carrier := s; op := $+; id := #0 |>; 1534 prod := <| carrier := s; op := $*; id := #1 |> 1535 |> 1536`; 1537(* overload set_to_ideal *) 1538val _ = overload_on("sideal", ``set_to_ideal r``); 1539 1540(* Theorem: Ring r ==> !z. z IN R ==> 1541 (set_to_ideal (PolyRing r) {p | poly p /\ root p z}) << (PolyRing r) *) 1542(* Proof: 1543 By ideal_def, set_to_ideal_def, this is to show: 1544 (1) <|carrier := {p | poly p /\ root p z}; op := $+; id := |0||> <= (PolyRing r).sum 1545 By Subgroup_def, this is to show: 1546 (1) Group <|carrier := {p | poly p /\ root p z}; op := $+; id := |0||> 1547 By group_def_alt, this is to show: 1548 (1) poly x /\ poly y ==> poly (x + y), true by poly_add_poly 1549 (2) root x z /\ root y z ==> root (x + y) z, true by 1550 (3) poly x /\ poly y /\ poly z' ==> x + y + z' = x + (y + z'), true by poly_add_assoc 1551 (4) poly |0|, true by poly_zero_poly 1552 (5) root |0| z, true by poly_root_zero 1553 (6) poly x ==> |0| + x = x, true by poly_add_lzero 1554 (7) poly x /\ root x z ==> ?y. (poly y /\ root y z) /\ (y + x = |0|) 1555 Let y = -x, then true by poly_root_neg 1556 (2) Group (PolyRing r).sum, true by poly_add_group 1557 (3) {p | poly p /\ root p z} SUBSET (PolyRing r).sum.carrier 1558 This is true by poly_ring_element, poly_ring_carriers, SUBSET_DEF. 1559 (2) x IN {p | poly p /\ root p z} /\ y IN (PolyRing r).carrier ==> x * y IN {p | poly p /\ root p z} 1560 or poly x /\ root p x /\ poly y ==> poly (x * y) /\ root (x * y) z 1561 This is true by poly_mult_poly, poly_root_mult. 1562 (3) x IN {p | poly p /\ root p z} /\ y IN (PolyRing r).carrier ==> y * x IN {p | poly p /\ root p z} 1563 or poly x /\ root p x /\ poly y ==> poly (x * y) /\ root (y * x) z 1564 This is true by poly_mult_poly, poly_root_mult_comm. 1565*) 1566val poly_root_poly_ideal = store_thm( 1567 "poly_root_poly_ideal", 1568 ``!r:'a ring. Ring r ==> !z. z IN R ==> 1569 (set_to_ideal (PolyRing r) {p | poly p /\ root p z}) << (PolyRing r)``, 1570 rw_tac std_ss[ideal_def, set_to_ideal_def, Subgroup_def, poly_ring_element, GSPECIFICATION] >| [ 1571 rw_tac std_ss[group_def_alt, GSPECIFICATION] >- 1572 rw[] >- 1573 rw[poly_root_add] >- 1574 rw[poly_add_assoc] >- 1575 rw[] >- 1576 rw[] >- 1577 rw[] >> 1578 metis_tac[poly_root_neg, poly_neg_poly, poly_add_lneg], 1579 rw[poly_add_group], 1580 rw[poly_ring_element, poly_ring_carriers, SUBSET_DEF], 1581 rw[], 1582 rw[poly_root_mult], 1583 rw[], 1584 rw[poly_root_mult_comm] 1585 ]); 1586 1587(* 1588Given an a which is algebraic over some subfield K of F, it can be checked (exercise!) 1589that the set J = {f IN K[x]: f(a) = 0} is an ideal of F[x] and J <> (0). By Theorem 3.4 1590it follows that there exists a uniquely determined monic polynomial g IN K[x] which 1591generates J, i.e. J = (g). 1592 1593Definition: call this the minimal polynomial of a over K. 1594We refer to the degree of a over K = deg g. 1595 1596type checking: 1597g `!r:'a ring. Ring r ==> !x. x IN R ==> sideal R << r`; 1598g `!r:'a ring. Ring r ==> !x. x IN R ==> set_to_ideal (PF r) Fp << (PF r)`; 1599g `!r:'a ring. Ring r ==> !x. x IN R ==> set_to_ideal (PF r) Fp << r`; 1600 1601g `!r:'a ring. Ring r ==> !x. x IN R ==> 1602 (set_to_ideal (PolyRing (PF r)) (PolyRing (PF r)).carrier << (PolyRing r))`; 1603g `!r:'a ring. Ring r ==> !z. z IN R ==> 1604 (set_to_ideal (PolyRing (PF r)) {p | pfpoly p /\ (root p z)}) << (PolyRing r)`; 1605*) 1606 1607(* ------------------------------------------------------------------------- *) 1608 1609(* export theory at end *) 1610val _ = export_theory(); 1611 1612(*===========================================================================*) 1613