src/HOL/Library/Polynomial_Factorial.thy
changeset 65389 6f9c6ae27984
parent 65366 10ca63a18e56
child 65390 83586780598b
equal deleted inserted replaced
65388:a8d868477bc0 65389:6f9c6ae27984
    14   Field_as_Ring
    14   Field_as_Ring
    15 begin
    15 begin
    16 
    16 
    17 subsection \<open>Various facts about polynomials\<close>
    17 subsection \<open>Various facts about polynomials\<close>
    18 
    18 
    19 lemma prod_mset_const_poly: "prod_mset (image_mset (\<lambda>x. [:f x:]) A) = [:prod_mset (image_mset f A):]"
    19 lemma prod_mset_const_poly: " (\<Prod>x\<in>#A. [:f x:]) = [:prod_mset (image_mset f A):]"
    20   by (induction A) (simp_all add: one_poly_def mult_ac)
    20   by (induct A) (simp_all add: one_poly_def ac_simps)
    21 
    21 
    22 lemma irreducible_const_poly_iff:
    22 lemma irreducible_const_poly_iff:
    23   fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
    23   fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
    24   shows "irreducible [:c:] \<longleftrightarrow> irreducible c"
    24   shows "irreducible [:c:] \<longleftrightarrow> irreducible c"
    25 proof
    25 proof
   167 lemma fract_poly_dvd: "p dvd q \<Longrightarrow> fract_poly p dvd fract_poly q"
   167 lemma fract_poly_dvd: "p dvd q \<Longrightarrow> fract_poly p dvd fract_poly q"
   168   by (auto elim!: dvdE)
   168   by (auto elim!: dvdE)
   169 
   169 
   170 lemma prod_mset_fract_poly: 
   170 lemma prod_mset_fract_poly: 
   171   "prod_mset (image_mset (\<lambda>x. fract_poly (f x)) A) = fract_poly (prod_mset (image_mset f A))"
   171   "prod_mset (image_mset (\<lambda>x. fract_poly (f x)) A) = fract_poly (prod_mset (image_mset f A))"
   172   by (induction A) (simp_all add: mult_ac)
   172   by (induct A) (simp_all add: one_poly_def ac_simps)
   173   
   173   
   174 lemma is_unit_fract_poly_iff:
   174 lemma is_unit_fract_poly_iff:
   175   "p dvd 1 \<longleftrightarrow> fract_poly p dvd 1 \<and> content p = 1"
   175   "p dvd 1 \<longleftrightarrow> fract_poly p dvd 1 \<and> content p = 1"
   176 proof safe
   176 proof safe
   177   assume A: "p dvd 1"
   177   assume A: "p dvd 1"
   178   with fract_poly_dvd[of p 1] show "is_unit (fract_poly p)" by simp
   178   with fract_poly_dvd [of p 1] show "is_unit (fract_poly p)"
       
   179     by simp
   179   from A show "content p = 1"
   180   from A show "content p = 1"
   180     by (auto simp: is_unit_poly_iff normalize_1_iff)
   181     by (auto simp: is_unit_poly_iff normalize_1_iff)
   181 next
   182 next
   182   assume A: "fract_poly p dvd 1" and B: "content p = 1"
   183   assume A: "fract_poly p dvd 1" and B: "content p = 1"
   183   from A obtain c where c: "fract_poly p = [:c:]" by (auto simp: is_unit_poly_iff)
   184   from A obtain c where c: "fract_poly p = [:c:]" by (auto simp: is_unit_poly_iff)