Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Algebra/Multiplicative_Group.thy
changeset 77061 5de3772609ea
parent 76987 4c275405faae 
--- a/src/HOL/Algebra/Multiplicative_Group.thy	Mon Jan 23 22:33:25 2023 +0100
+++ b/src/HOL/Algebra/Multiplicative_Group.thy	Tue Jan 24 10:30:56 2023 +0000
@@ -533,8 +533,7 @@
         using n
         by simp (metis (no_types, lifting) assms dvd_minus_mod dvd_trans int_pow_eq int_pow_eq_id int_pow_int)
       show "nat (a mod int n) \<in> {0..<n}"
-        using n  apply (simp add:  split: split_nat)
-        using Euclidean_Division.pos_mod_bound by presburger
+        using n by (simp add: nat_less_iff)
     qed
     then have "carrier (subgroup_generated G {x}) \<subseteq> ([^]) x ` {0..<n}"
       using carrier_subgroup_generated_by_singleton [OF assms] by auto
isabelle