QE による検証
Mathematica の QE のデフォルトの議論領域は
Reduce[Exists[x, a*x^2 == 1]]
に対する出力
からも判るように複素数体であり,前回公開した Mathematica での実装の目的の 1 つは,この QE による結果の検証でした.
Mathematica で前回の各関数の定義コードを実行した後,例えば,
(p1=PL[[1]])@x
を
mp[p1];nGG[];cs[];RR[];InputForm@DP
のように処理すると
といった出力が得られます.
このとき,A についての 2 つの条件
(1) A が分解体の primitive element の定義多項式 p2 の零となる
(2) A の多項式で表された根全体 r1 /. pe -> A が入力の多項式 p1 の根全体となる
が等価であるという式
ForAll[A, Equivalent[p2@A == 0, ForAll[x, Times @@ (x - r1 /. pe -> A) == p1@x]]]
すなわち
を複素数体上で
Reduce[%,Complexes]
のように QE すると
と答えてくれます.
また,A についての 2 つの条件
(1) A が分解体の primitive element の定義多項式 p2 の零となる
(3) 出力 DP に属する全ての多項式の共通の零点 (w,e[1]) が存在する
が等価であるという式
ForAll[A, Equivalent[p2@A == 0, Exists[Evaluate@Rest@vs, And @@ (# == 0 & /@ DP)]]]
すなわち
を複素数体上で
Reduce[%,Complexes]
のように QE すると
と答えてくれます.