equal
deleted
inserted
replaced
1450 |
1450 |
1451 lemma lcm_0_iff_nat[simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0" |
1451 lemma lcm_0_iff_nat[simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0" |
1452 by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat) |
1452 by (metis lcm_0_left_nat lcm_0_nat mult_is_0 prod_gcd_lcm_nat) |
1453 |
1453 |
1454 lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0" |
1454 lemma lcm_0_iff_int[simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0" |
1455 by (metis lcm_0_int lcm_0_left_int lcm_pos_int zless_le) |
1455 by (metis lcm_0_int lcm_0_left_int lcm_pos_int less_le) |
1456 |
1456 |
1457 lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1" |
1457 lemma lcm_1_iff_nat[simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1" |
1458 by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat) |
1458 by (metis gcd_1_nat lcm_unique_nat nat_mult_1 prod_gcd_lcm_nat) |
1459 |
1459 |
1460 lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)" |
1460 lemma lcm_1_iff_int[simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)" |