changeset 64850 | fc9265882329 |
parent 64848 | c50db2128048 |
child 64860 | 4d56170d97b3 |
64849:766db3539859 | 64850:fc9265882329 |
---|---|
979 lemma lcm_poly_code [code]: |
979 lemma lcm_poly_code [code]: |
980 fixes p q :: "'a :: factorial_ring_gcd poly" |
980 fixes p q :: "'a :: factorial_ring_gcd poly" |
981 shows "lcm p q = normalize (p * q) div gcd p q" |
981 shows "lcm p q = normalize (p * q) div gcd p q" |
982 by (fact lcm_gcd) |
982 by (fact lcm_gcd) |
983 |
983 |
984 declare Gcd_set |
984 lemmas Gcd_poly_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"] |
985 [where ?'a = "'a :: factorial_ring_gcd poly", code] |
985 lemmas Lcm_poly_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"] |
986 |
986 |
987 declare Lcm_set |
|
988 [where ?'a = "'a :: factorial_ring_gcd poly", code] |
|
989 |
|
990 text \<open>Example: |
987 text \<open>Example: |
991 @{lemma "Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]" by eval} |
988 @{lemma "Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]" by eval} |
992 \<close> |
989 \<close> |
993 |
990 |
994 end |
991 end |