(* File: Min_Int_Poly.thy Author: Manuel Eberl, TU München *) section ‹The minimal polynomial of an algebraic number› theory Min_Int_Poly imports Algebraic_Numbers_Prelim begin text ‹ Given an algebraic number ‹x› in a field, the minimal polynomial is the unique irreducible integer polynomial with positive leading coefficient that has ‹x› as a root. Note that we assume characteristic 0 since the material upon which all of this builds also assumes it. › definition min_int_poly :: "'a :: field_char_0 ⇒ int poly" where "min_int_poly x = (if algebraic x then THE p. p represents x ∧ irreducible p ∧ lead_coeff p > 0 else [:0, 1:])" lemma fixes x :: "'a :: {field_char_0, field_gcd}" shows min_int_poly_represents [intro]: "algebraic x ⟹ min_int_poly x represents x" and min_int_poly_irreducible [intro]: "irreducible (min_int_poly x)" and lead_coeff_min_int_poly_pos: "lead_coeff (min_int_poly x) > 0" proof - note * = theI'[OF algebraic_imp_represents_unique, of x] show "min_int_poly x represents x" if "algebraic x" using *[OF that] by (simp add: that min_int_poly_def) have "irreducible [:0, 1::int:]" by (rule irreducible_linear_poly) auto thus "irreducible (min_int_poly x)" using * by (auto simp: min_int_poly_def) show "lead_coeff (min_int_poly x) > 0" using * by (auto simp: min_int_poly_def) qed lemma fixes x :: "'a :: {field_char_0, field_gcd}" shows degree_min_int_poly_pos [intro]: "degree (min_int_poly x) > 0" and degree_min_int_poly_nonzero [simp]: "degree (min_int_poly x) ≠ 0" proof - show "degree (min_int_poly x) > 0" proof (cases "algebraic x") case True hence "min_int_poly x represents x" by auto thus ?thesis by blast qed (auto simp: min_int_poly_def) thus "degree (min_int_poly x) ≠ 0" by blast qed lemma min_int_poly_primitive [intro]: fixes x :: "'a :: {field_char_0, field_gcd}" shows "primitive (min_int_poly x)" by (rule irreducible_imp_primitive) auto lemma min_int_poly_content [simp]: fixes x :: "'a :: {field_char_0, field_gcd}" shows "content (min_int_poly x) = 1" using min_int_poly_primitive[of x] by (simp add: primitive_def) lemma ipoly_min_int_poly [simp]: "algebraic x ⟹ ipoly (min_int_poly x) (x :: 'a :: {field_gcd, field_char_0}) = 0" using min_int_poly_represents[of x] by (auto simp: represents_def) lemma min_int_poly_nonzero [simp]: fixes x :: "'a :: {field_char_0, field_gcd}" shows "min_int_poly x ≠ 0" using lead_coeff_min_int_poly_pos[of x] by auto lemma min_int_poly_normalize [simp]: fixes x :: "'a :: {field_char_0, field_gcd}" shows "normalize (min_int_poly x) = min_int_poly x" unfolding normalize_poly_def using lead_coeff_min_int_poly_pos[of x] by simp lemma min_int_poly_prime_elem [intro]: fixes x :: "'a :: {field_char_0, field_gcd}" shows "prime_elem (min_int_poly x)" using min_int_poly_irreducible[of x] by blast lemma min_int_poly_prime [intro]: fixes x :: "'a :: {field_char_0, field_gcd}" shows "prime (min_int_poly x)" using min_int_poly_prime_elem[of x] by (simp only: prime_normalize_iff [symmetric] min_int_poly_normalize) lemma min_int_poly_unique: fixes x :: "'a :: {field_char_0, field_gcd}" assumes "p represents x" "irreducible p" "lead_coeff p > 0" shows "min_int_poly x = p" proof - from assms(1) have x: "algebraic x" using algebraic_iff_represents by blast thus ?thesis using the1_equality[OF algebraic_imp_represents_unique[OF x], of p] assms unfolding min_int_poly_def by auto qed lemma min_int_poly_of_int [simp]: "min_int_poly (of_int n :: 'a :: {field_char_0, field_gcd}) = [:-of_int n, 1:]" by (intro min_int_poly_unique irreducible_linear_poly) auto lemma min_int_poly_of_nat [simp]: "min_int_poly (of_nat n :: 'a :: {field_char_0, field_gcd}) = [:-of_nat n, 1:]" using min_int_poly_of_int[of "int n"] by (simp del: min_int_poly_of_int) lemma min_int_poly_0 [simp]: "min_int_poly (0 :: 'a :: {field_char_0, field_gcd}) = [:0, 1:]" using min_int_poly_of_int[of 0] unfolding of_int_0 by simp lemma min_int_poly_1 [simp]: "min_int_poly (1 :: 'a :: {field_char_0, field_gcd}) = [:-1, 1:]" using min_int_poly_of_int[of 1] unfolding of_int_1 by simp lemma poly_min_int_poly_0_eq_0_iff [simp]: fixes x :: "'a :: {field_char_0, field_gcd}" assumes "algebraic x" shows "poly (min_int_poly x) 0 = 0 ⟷ x = 0" proof assume *: "poly (min_int_poly x) 0 = 0" show "x = 0" proof (rule ccontr) assume "x ≠ 0" hence "poly (min_int_poly x) 0 ≠ 0" using assms by (intro represents_irr_non_0) auto with * show False by contradiction qed qed auto lemma min_int_poly_eqI: fixes x :: "'a :: {field_char_0, field_gcd}" assumes "p represents x" "irreducible p" "lead_coeff p ≥ 0" shows "min_int_poly x = p" proof - from assms have [simp]: "p ≠ 0" by auto have "lead_coeff p ≠ 0" by auto with assms(3) have "lead_coeff p > 0" by linarith moreover have "algebraic x" using ‹p represents x› by (meson algebraic_iff_represents) ultimately show ?thesis unfolding min_int_poly_def using the1_equality[OF algebraic_imp_represents_unique[OF ‹algebraic x›], of p] assms by auto qed text ‹Implementation for real and rational numbers› lemma min_int_poly_of_rat: "min_int_poly (of_rat r :: 'a :: {field_char_0, field_gcd}) = poly_rat r" by (intro min_int_poly_unique, auto) definition min_int_poly_real :: "real ⇒ int poly" where [simp]: "min_int_poly_real = min_int_poly" lemma min_int_poly_real_code_unfold [code_unfold]: "min_int_poly = min_int_poly_real" by simp lemma min_int_poly_real_basic_impl[code]: "min_int_poly_real (real_of_rat x) = poly_rat x" unfolding min_int_poly_real_def by (rule min_int_poly_of_rat) lemma min_int_poly_rat_code_unfold [code_unfold]: "min_int_poly = poly_rat" by (intro ext, insert min_int_poly_of_rat[where ?'a = rat], auto) end