changeset 64860 | 4d56170d97b3 |
parent 64850 | fc9265882329 |
child 64911 | f0e07600de47 |
64859:e600cfdc9e97 | 64860:4d56170d97b3 |
---|---|
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 lemmas Gcd_poly_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"] |
984 lemmas Gcd_poly_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"] |
985 lemmas Lcm_poly_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"] |
985 lemmas Lcm_poly_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"] |
986 |
986 |
987 text \<open>Example: |
987 text \<open>Example: |
988 @{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} |
989 \<close> |
989 \<close> |
990 |
990 |
991 end |
991 end |