Theory Polynomial_Factorization.Polynomial_Irreducibility
section ‹Polynomial Divisibility›
text ‹We make a connection between irreducibility of Missing-Polynomial and Factorial-Ring.›
theory Polynomial_Irreducibility
imports
Polynomial_Interpolation.Missing_Polynomial
begin
lemma dvd_gcd_mult: fixes p :: "'a :: semiring_gcd"
assumes dvd: "k dvd p * q" "k dvd p * r"
shows "k dvd p * gcd q r"
by (rule dvd_trans, rule gcd_greatest[OF dvd])
(auto intro!: mult_dvd_mono simp: gcd_mult_left)
lemma poly_gcd_monic_factor:
"monic p ⟹ gcd (p * q) (p * r) = p * gcd q r"
by (rule gcdI [symmetric]) (simp_all add: normalize_mult normalize_monic dvd_gcd_mult)
context
assumes "SORT_CONSTRAINT('a :: field)"
begin
lemma field_poly_irreducible_dvd_mult[simp]:
assumes irr: "irreducible (p :: 'a poly)"
shows "p dvd q * r ⟷ p dvd q ∨ p dvd r"
using field_poly_irreducible_imp_prime[OF irr] by (simp add: prime_elem_dvd_mult_iff)
lemma irreducible_dvd_pow:
fixes p :: "'a poly"
assumes irr: "irreducible p"
shows "p dvd q ^ n ⟹ p dvd q"
using field_poly_irreducible_imp_prime[OF irr] by (rule prime_elem_dvd_power)
lemma irreducible_dvd_prod: fixes p :: "'a poly"
assumes irr: "irreducible p"
and dvd: "p dvd prod f as"
shows "∃ a ∈ as. p dvd f a"
by (insert dvd, induct as rule: infinite_finite_induct, insert irr, auto)
lemma irreducible_dvd_prod_list: fixes p :: "'a poly"
assumes irr: "irreducible p"
and dvd: "p dvd prod_list as"
shows "∃ a ∈ set as. p dvd a"
by (insert dvd, induct as, insert irr, auto)
lemma dvd_mult_imp_degree: fixes p :: "'a poly"
assumes "p dvd q * r"
and "degree p > 0"
shows "∃ s t. irreducible s ∧ p = s * t ∧ (s dvd q ∨ s dvd r)"
proof -
from irreducible⇩d_factor[OF assms(2)] obtain s t
where irred: "irreducible s" and p: "p = s * t" by auto
from ‹p dvd q * r› p have s: "s dvd q * r" unfolding dvd_def by auto
from s p irred show ?thesis by auto
qed
end
end