src/HOL/Number_Theory/Residues.thy
changeset 36350 bc7982c54e37
parent 35416 d8d7d1b785af
child 41541 1fa4725c4656
equal deleted inserted replaced
36349:39be26d1bc28 36350:bc7982c54e37
    67   apply (rule comm_monoid)
    67   apply (rule comm_monoid)
    68   apply (unfold R_def residue_ring_def, auto)
    68   apply (unfold R_def residue_ring_def, auto)
    69   apply (subst mod_add_eq [symmetric])
    69   apply (subst mod_add_eq [symmetric])
    70   apply (subst mult_commute)
    70   apply (subst mult_commute)
    71   apply (subst zmod_zmult1_eq [symmetric])
    71   apply (subst zmod_zmult1_eq [symmetric])
    72   apply (simp add: ring_simps)
    72   apply (simp add: field_simps)
    73 done
    73 done
    74 
    74 
    75 end
    75 end
    76 
    76 
    77 sublocale residues < cring
    77 sublocale residues < cring