equal
deleted
inserted
replaced
134 fixes n p :: nat |
134 fixes n p :: nat |
135 assumes "p > 0" "n dvd p" |
135 assumes "p > 0" "n dvd p" |
136 shows "n > 0 \<and> n \<le> p" |
136 shows "n > 0 \<and> n \<le> p" |
137 using assms by (simp add: dvd_pos_nat dvd_imp_le) |
137 using assms by (simp add: dvd_pos_nat dvd_imp_le) |
138 |
138 |
139 (* Deviates from the definition given in the library in number theory *) |
139 (* TODO FIXME: This is the "totient" function from HOL-Number_Theory, but since part of |
|
140 HOL-Number_Theory depends on HOL-Algebra.Multiplicative_Group, there would be a cyclic |
|
141 dependency. *) |
140 definition phi' :: "nat => nat" |
142 definition phi' :: "nat => nat" |
141 where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m}" |
143 where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m}" |
142 |
144 |
143 notation (latex output) |
145 notation (latex output) |
144 phi' ("\<phi> _") |
146 phi' ("\<phi> _") |