src/HOL/Number_Theory/Residues.thy
changeset 65899 ab7d8c999531
parent 65726 f5d64d094efe
child 66304 cde6ceffcbc7
equal deleted inserted replaced
65898:f02a1289e2c6 65899:ab7d8c999531
    55     with m_gt_one that show ?thesis
    55     with m_gt_one that show ?thesis
    56       by (metis False atLeastAtMost_iff diff_ge_0_iff_ge diff_left_mono int_one_le_iff_zero_less less_le)
    56       by (metis False atLeastAtMost_iff diff_ge_0_iff_ge diff_left_mono int_one_le_iff_zero_less less_le)
    57   qed
    57   qed
    58   with m_gt_one show ?thesis
    58   with m_gt_one show ?thesis
    59     by (fastforce simp add: R_def residue_ring_def mod_add_right_eq ac_simps  intro!: abelian_groupI)
    59     by (fastforce simp add: R_def residue_ring_def mod_add_right_eq ac_simps  intro!: abelian_groupI)
    60 qed    
    60 qed
    61 
    61 
    62 lemma comm_monoid: "comm_monoid R"
    62 lemma comm_monoid: "comm_monoid R"
    63   unfolding R_def residue_ring_def
    63   unfolding R_def residue_ring_def
    64   apply (rule comm_monoidI)
    64   apply (rule comm_monoidI)
    65     using m_gt_one  apply auto
    65     using m_gt_one  apply auto
   245 
   245 
   246 subsection \<open>Euler's theorem\<close>
   246 subsection \<open>Euler's theorem\<close>
   247 
   247 
   248 lemma (in residues) totient_eq:
   248 lemma (in residues) totient_eq:
   249   "totient (nat m) = card (Units R)"
   249   "totient (nat m) = card (Units R)"
   250   thm R_def
       
   251 proof -
   250 proof -
   252   have *: "inj_on nat (Units R)"
   251   have *: "inj_on nat (Units R)"
   253     by (rule inj_onI) (auto simp add: res_units_eq)
   252     by (rule inj_onI) (auto simp add: res_units_eq)
   254   define m' where "m' = nat m"
   253   define m' where "m' = nat m"
   255   from m_gt_one have m: "m = int m'" "m' > 1" by (simp_all add: m'_def)
   254   from m_gt_one have m: "m = int m'" "m' > 1" by (simp_all add: m'_def)