equal
deleted
inserted
replaced
37 by (blast intro: relprime_dvd_mult prime_imp_relprime) |
37 by (blast intro: relprime_dvd_mult prime_imp_relprime) |
38 |
38 |
39 lemma prime_dvd_square: "prime p ==> p dvd m^Suc (Suc 0) ==> p dvd m" |
39 lemma prime_dvd_square: "prime p ==> p dvd m^Suc (Suc 0) ==> p dvd m" |
40 by (auto dest: prime_dvd_mult) |
40 by (auto dest: prime_dvd_mult) |
41 |
41 |
42 lemma prime_dvd_power_two: "prime p ==> p dvd m\<twosuperior> ==> p dvd m" |
42 lemma prime_dvd_power_two: "prime p ==> p dvd m\<^sup>2 ==> p dvd m" |
43 by (rule prime_dvd_square) (simp_all add: power2_eq_square) |
43 by (rule prime_dvd_square) (simp_all add: power2_eq_square) |
44 |
44 |
45 |
45 |
46 lemma exp_eq_1:"(x::nat)^n = 1 \<longleftrightarrow> x = 1 \<or> n = 0" |
46 lemma exp_eq_1:"(x::nat)^n = 1 \<longleftrightarrow> x = 1 \<or> n = 0" |
47 by (induct n, auto) |
47 by (induct n, auto) |