--- a/src/HOL/Number_Theory/Totient.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Number_Theory/Totient.thy Wed Jan 10 15:25:09 2018 +0100
@@ -215,7 +215,7 @@
using \<open>n > 0\<close> by (intro card_UN_disjoint) (auto simp: A_def)
also have "\<dots> = (\<Sum>d | d dvd n. totient (n div d))" by (intro sum.cong refl *) auto
also have "\<dots> = (\<Sum>d | d dvd n. totient d)" using \<open>n > 0\<close>
- by (intro sum.reindex_bij_witness[of _ "op div n" "op div n"]) (auto elim: dvdE)
+ by (intro sum.reindex_bij_witness[of _ "(div) n" "(div) n"]) (auto elim: dvdE)
finally show ?thesis ..
qed auto
@@ -239,11 +239,11 @@
assumes "prime p"
shows "totient (p ^ Suc n) = p ^ n * (p - 1)"
proof -
- from assms have "totient (p ^ Suc n) = card ({0<..p ^ Suc n} - op * p ` {0<..p ^ n})"
+ from assms have "totient (p ^ Suc n) = card ({0<..p ^ Suc n} - ( * ) p ` {0<..p ^ n})"
unfolding totient_def by (subst totatives_prime_power_Suc) simp_all
- also from assms have "\<dots> = p ^ Suc n - card (op * p ` {0<..p^n})"
+ also from assms have "\<dots> = p ^ Suc n - card (( * ) p ` {0<..p^n})"
by (subst card_Diff_subset) (auto intro: prime_gt_0_nat)
- also from assms have "card (op * p ` {0<..p^n}) = p ^ n"
+ also from assms have "card (( * ) p ` {0<..p^n}) = p ^ n"
by (subst card_image) (auto simp: inj_on_def)
also have "p ^ Suc n - p ^ n = p ^ n * (p - 1)" by (simp add: algebra_simps)
finally show ?thesis .