equal
deleted
inserted
replaced
7 *) |
7 *) |
8 |
8 |
9 theory Polynomial_Factorial |
9 theory Polynomial_Factorial |
10 imports |
10 imports |
11 Complex_Main |
11 Complex_Main |
12 "~~/src/HOL/Library/Polynomial" |
12 Polynomial |
13 "~~/src/HOL/Library/Normalized_Fraction" |
13 Normalized_Fraction |
14 "~~/src/HOL/Library/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_mset (image_mset (\<lambda>x. [:f x:]) A) = [:prod_mset (image_mset f A):]" |