Minor update to documentation of splitting fields.

HOL-Theorem-Prover · Oct 19, 2022 · d0be848 · d0be848
1 parent a80adae
commit d0be848
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/examples/algebra/finitefield/ffSplitScript.sml b/examples/algebra/finitefield/ffSplitScript.sml
@@ -326,7 +326,7 @@ open GaussTheory; (* for divisors *)
    poly_mini_root_order            |- !r s. FiniteField r /\ s <<= r ==> !n. n divides CARD R+ ==>
                                       !x. x IN R /\ root (mini n) x ==> (forder x = n)
 
-   Cyclotomic Factorisation of Unity Polynomial (old):
+   Another Cyclotomic Factorisation of Unity Polynomial:
    poly_unity_splitting_field_exists
                                    |- !r n. FiniteField r /\ coprime n (CARD R) ==>
                                       ?t st. FiniteField t /\ st <<= t /\ FieldIso (\e. up e) r st /\
@@ -2685,9 +2685,11 @@ val poly_mini_root_order = store_thm(
   metis_tac[poly_minimal_root_order, poly_mini_def]);
 
 (* ------------------------------------------------------------------------- *)
-(* Cyclotomic Factorisation of Unity Polynomial (old)                        *)
+(* Another Cyclotomic Factorisation of Unity Polynomial                      *)
 (* ------------------------------------------------------------------------- *)
 
+(* Note: this is the original approach. *)
+
 (*
 poly_unity_eq_poly_cyclo_product;
 |- !r. FiniteField r ==> !n. n divides CARD R+ ==> (unity n = PPIMAGE cyclo (divisors n))