Theory ERF_Library
theory ERF_Library
imports
Mason_Stothers.Mason_Stothers
Berlekamp_Zassenhaus.Berlekamp_Type_Based
Perfect_Fields.Perfect_Fields
begin
hide_const (open) Formal_Power_Series.radical
section ‹Auxiliary Lemmas›
text ‹If all factors are monic, the product is monic as well (i.e.\ the normalization is itself).›
lemma normalize_prod_monics:
assumes "∀x∈A. monic x"
shows "normalize (∏x∈A. x^(e x)) = (∏x∈A. x^(e x))"
by (simp add: assms monic_power monic_prod normalize_monic)
text ‹All primes are monic.›
lemma prime_monic:
fixes p :: "'a :: {euclidean_ring_gcd,field} poly"
assumes "p≠0" "prime p" shows "monic p"
using normalize_prime[OF assms(2)] monic_normalize[OF assms(1)] by auto
text ‹If we know the factorization of a polynomial, we can explicitly characterize the derivative
of said polynomial.›
lemma pderiv_exp_prod_monic:
assumes "p = prod_mset fs"
shows "pderiv p = (sum (λ fi. let ei = count fs fi in
Polynomial.smult (of_nat ei) (pderiv fi) * fi^(ei-1) * prod (λ fj. fj^(count fs fj))
((set_mset fs) - {fi})) (set_mset fs))"
proof -
have pderiv_fi: "pderiv (fi ^ count fs fi) =
Polynomial.smult (of_nat (count fs fi)) (pderiv fi * (fi ^ (count fs fi - Suc 0)))"
if "fi ∈# fs" for fi
proof -
obtain i where i: "Suc i = count fs fi" by (metis ‹fi ∈# fs› in_countE)
show ?thesis unfolding i[symmetric] by (subst pderiv_power_Suc) (auto simp add: algebra_simps)
qed
show ?thesis unfolding assms prod_mset_multiplicity pderiv_prod sum_distrib_left Let_def
by (rule sum.cong[OF refl]) (auto simp add: algebra_simps pderiv_fi)
qed
text ‹Any element that divides a prime is either congruent to the prime (i.e.\ ‹p dvd c›) or
a unit itself. Careful: This does not mean that $p=c$ since there could be another unit $u$ such
that $p = u*c$.›
lemma prime_factors_prime:
assumes "c dvd p" "prime p"
shows "is_unit c ∨ p dvd c"
using assms unfolding normalization_semidom_class.prime_def
by (meson prime_elemD2)
text ‹A prime polynomial has degree greater than zero. This is clear since any polynomial of
degree 0 is constant and thus also a unit.›
lemma prime_degree_gt_zero:
fixes p::"'a::{idom_divide,semidom_divide_unit_factor,field} poly"
assumes "prime p"
shows "degree p > 0"
using assms by fastforce
text ‹This lemma helps to reason that if a sum is zero, under some conditions we can follow that
the summands must also be zero.›
lemma one_summand_zero:
fixes a2::"'a ::field poly"
assumes "Polynomial.smult a1 a2 + b = 0""c dvd b" "¬ c dvd a2"
shows "a1 = 0"
by (metis assms dvd_0_right dvd_add_triv_right_iff dvd_smult_cancel dvd_trans)
subsection ‹Lemmas for the ‹radical› of polynomials›
text ‹Properties of the function ‹radical›.
Note: The radical polynomial in algebra denotes something else. Here, ‹radical› denotes the
square-free and monic part of a polynomial (i.e.\ the product of all prime factors). This notion
corresponds to radical ideals generated by square-free polynomials.›
lemma squarefree_radical [intro]: "f ≠ 0 ⟹ squarefree (radical f)"
by (simp add: in_prime_factors_iff multiplicity_radical_prime squarefree_factorial_semiring')
lemma (in normalization_semidom_multiplicative) normalize_prod:
"normalize (∏x∈A. f (x :: 'b) :: 'a) = (∏x∈A. normalize (f x))"
by (induction A rule: infinite_finite_induct) (auto simp: normalize_mult)
lemma normalize_radical [simp]:
fixes f :: "'a :: factorial_semiring_multiplicative"
shows "normalize (radical f) = radical f"
by (auto simp: radical_def normalize_prod in_prime_factors_iff normalize_prime intro!: prod.cong)
lemma radical_of_squarefree:
assumes "squarefree f"
shows "normalize (radical f) = normalize f"
proof -
from assms have [simp]: "f ≠ 0"
by auto
have "normalize (∏⇩# (prime_factorization f)) = normalize f"
by (intro prod_mset_prime_factorization_weak) auto
also have "prime_factorization f = mset_set (prime_factors f)"
using assms
by (intro multiset_eqI)
(auto simp: count_prime_factorization count_mset_set' squarefree_factorial_semiring'
in_prime_factors_iff not_dvd_imp_multiplicity_0)
also have "prod_mset (mset_set (prime_factors f)) = radical f"
by (simp add: radical_def prod_unfold_prod_mset)
finally show ?thesis
by simp
qed
text ‹A constant polynomial has no primes in its prime factorization and its radical is 1. ›
lemma prime_factorization_degree0:
fixes f :: "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize,field} poly"
assumes "degree f = 0"
shows "prime_factorization f = {#}"
by (simp add: assms prime_factorization_empty_iff)
lemma prime_factors_degree0:
fixes f :: "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize,field} poly"
assumes "degree f = 0" "f≠0"
shows "prime_factors f = {}"
using prime_factorization_degree0 assms by auto
lemma radical_degree0:
fixes f :: "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize,field} poly"
assumes "degree f = 0" "f≠0"
shows "radical f = 1"
by (simp add: assms is_unit_iff_degree)
text ‹A polynomial is square-free iff its normalization is also square-free.›
lemma squarefree_normalize:
"squarefree f ⟷ squarefree (normalize f)"
by (simp add: squarefree_def)
text ‹Important: The zeros of a polynomial are also zeros of its ‹radical› and vice versa.›
lemma same_zeros_radical: "(poly f a = 0) = (poly (radical f) a = 0)"
proof (cases "f = 0")
case True show ?thesis unfolding True radical_def by auto
next
case False
have fin: "finite (prime_factors f)" by simp
have f: "f = unit_factor f * prod_mset (prime_factorization f)"
by (metis False in_prime_factors_imp_prime normalize_prime normalized_prod_msetI
prod_mset_prime_factorization_weak unit_factor_mult_normalize)
have "poly (unit_factor f) a≠0" using False poly_zero by fastforce
moreover have "((∏p∈#prime_factorization f. poly p a) = 0)=((∏k∈prime_factors f. poly k a) = 0)"
by (subst prod_mset_zero_iff,subst prod_zero_iff[OF fin]) auto
ultimately have "(poly f a = 0) = (poly (∏(prime_factors f)) a = 0)"
by (subst f, subst poly_prod, subst poly_mult, subst poly_hom.hom_prod_mset) auto
then show ?thesis unfolding radical_def using False by auto
qed
subsection ‹More on square-free polynomials›
text ‹We need to relate two different versions of the definition of a square-free polynomial
(i.e.\ the functions ‹squarefree› and ‹square_free›). Over fields, they differ only in their
behavior at $0$.)›
lemma squarefree_square_free:
fixes x :: "'a :: {field} poly"
assumes "x ≠ 0"
shows "squarefree x = square_free x"
using assms unfolding squarefree_def square_free_def proof (safe, goal_cases)
case (1 q)
have "q dvd 1" using 1(2,4) by (metis power2_eq_square)
then have "degree q = 0" using poly_dvd_1[of q] by auto
then show ?case using 1(3) by auto
next
case (2 y)
then have "degree y = 0" by (metis bot_nat_0.not_eq_extremum power2_eq_square)
have "y≠0" using 2(2,4) by fastforce
show ?case using is_unit_iff_degree[OF ‹y≠0›] ‹degree y = 0› by auto
qed
lemma (in comm_monoid_mult) prod_list_distinct_conv_prod_set:
"distinct xs ⟹ prod_list (map (f :: 'b ⇒ 'a) xs) = prod f (set xs)"
by (simp add: local.prod.distinct_set_conv_list)
lemma (in comm_monoid_mult) interv_prod_list_conv_prod_set_nat:
"prod_list (map (f :: nat ⇒ 'a) [m..<n]) = prod f (set [m..<n])"
by (metis distinct_upt local.prod.distinct_set_conv_list)
lemma (in comm_monoid_mult) prod_list_prod_nth:
"prod_list (xs :: 'a list) = (∏ i = 0 ..< length xs. xs ! i)"
using interv_prod_list_conv_prod_set_nat [of "(!) xs" 0 "length xs"] by (simp add: map_nth)
lemma squarefree_mult_imp_coprime [dest]:
assumes "squarefree (x * y)"
shows "coprime x y"
proof (rule coprimeI)
fix d assume "d dvd x" "d dvd y"
hence "d ^ 2 dvd x * y"
by (simp add: mult_dvd_mono power2_eq_square)
thus "d dvd 1"
using assms unfolding squarefree_def by blast
qed
end