--- a/src/HOL/Number_Theory/Residues.thy Mon May 22 11:34:42 2017 +0200
+++ b/src/HOL/Number_Theory/Residues.thy Mon May 22 14:08:22 2017 +0200
@@ -57,7 +57,7 @@
qed
with m_gt_one show ?thesis
by (fastforce simp add: R_def residue_ring_def mod_add_right_eq ac_simps intro!: abelian_groupI)
-qed
+qed
lemma comm_monoid: "comm_monoid R"
unfolding R_def residue_ring_def
@@ -247,7 +247,6 @@
lemma (in residues) totient_eq:
"totient (nat m) = card (Units R)"
- thm R_def
proof -
have *: "inj_on nat (Units R)"
by (rule inj_onI) (auto simp add: res_units_eq)