src/HOL/Library/Polynomial_Factorial.thy
 changeset 65389 6f9c6ae27984 parent 65366 10ca63a18e56 child 65390 83586780598b
equal 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)`