equal
deleted
inserted
replaced
83 |
83 |
84 definition lcm_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
84 definition lcm_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
85 where |
85 where |
86 "lcm_eucl a b = normalize (a * b) div gcd_eucl a b" |
86 "lcm_eucl a b = normalize (a * b) div gcd_eucl a b" |
87 |
87 |
88 definition Lcm_eucl :: "'a set \<Rightarrow> 'a" -- \<open> |
88 definition Lcm_eucl :: "'a set \<Rightarrow> 'a" \<comment> \<open> |
89 Somewhat complicated definition of Lcm that has the advantage of working |
89 Somewhat complicated definition of Lcm that has the advantage of working |
90 for infinite sets as well\<close> |
90 for infinite sets as well\<close> |
91 where |
91 where |
92 "Lcm_eucl A = (if \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) then |
92 "Lcm_eucl A = (if \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) then |
93 let l = SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = |
93 let l = SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = |