equal
deleted
inserted
replaced
1419 by (subst nat_lcm_commute, rule nat_lcm_dvd1) |
1419 by (subst nat_lcm_commute, rule nat_lcm_dvd1) |
1420 |
1420 |
1421 lemma int_lcm_dvd2 [iff]: "(n::int) dvd lcm m n" |
1421 lemma int_lcm_dvd2 [iff]: "(n::int) dvd lcm m n" |
1422 by (subst int_lcm_commute, rule int_lcm_dvd1) |
1422 by (subst int_lcm_commute, rule int_lcm_dvd1) |
1423 |
1423 |
|
1424 lemma dvd_lcm_if_dvd1_nat: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n" |
|
1425 by(metis nat_lcm_dvd1 dvd_trans) |
|
1426 |
|
1427 lemma dvd_lcm_if_dvd2_nat: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n" |
|
1428 by(metis nat_lcm_dvd2 dvd_trans) |
|
1429 |
|
1430 lemma dvd_lcm_if_dvd1_int: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n" |
|
1431 by(metis int_lcm_dvd1 dvd_trans) |
|
1432 |
|
1433 lemma dvd_lcm_if_dvd2_int: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n" |
|
1434 by(metis int_lcm_dvd2 dvd_trans) |
|
1435 |
1424 lemma nat_lcm_unique: "(a::nat) dvd d \<and> b dvd d \<and> |
1436 lemma nat_lcm_unique: "(a::nat) dvd d \<and> b dvd d \<and> |
1425 (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b" |
1437 (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b" |
1426 by (auto intro: dvd_anti_sym nat_lcm_least) |
1438 by (auto intro: dvd_anti_sym nat_lcm_least) |
1427 |
1439 |
1428 lemma int_lcm_unique: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and> |
1440 lemma int_lcm_unique: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and> |