equal
deleted
inserted
replaced
24 *) |
24 *) |
25 |
25 |
26 section \<open>Congruence\<close> |
26 section \<open>Congruence\<close> |
27 |
27 |
28 theory Cong |
28 theory Cong |
29 imports Primes |
29 imports "~~/src/HOL/Computational_Algebra/Primes" |
30 begin |
30 begin |
31 |
31 |
32 subsection \<open>Turn off \<open>One_nat_def\<close>\<close> |
32 subsection \<open>Turn off \<open>One_nat_def\<close>\<close> |
33 |
33 |
34 lemma power_eq_one_eq_nat [simp]: "((x::nat)^m = 1) = (m = 0 | x = 1)" |
34 lemma power_eq_one_eq_nat [simp]: "((x::nat)^m = 1) = (m = 0 | x = 1)" |