src/HOL/GCD.thy
changeset 64272 f76b6dda2e56
parent 64242 93c6f0da5c70
child 64591 240a39af9ec4
     1.1 --- a/src/HOL/GCD.thy	Mon Oct 17 14:37:32 2016 +0200
     1.2 +++ b/src/HOL/GCD.thy	Mon Oct 17 17:33:07 2016 +0200
     1.3 @@ -859,7 +859,7 @@
     1.4  lemma coprime_plus_one [simp]: "gcd (n + 1) n = 1"
     1.5    by (subst add_commute) simp
     1.6  
     1.7 -lemma setprod_coprime [rule_format]: "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
     1.8 +lemma prod_coprime [rule_format]: "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
     1.9    by (induct A rule: infinite_finite_induct) (auto simp add: gcd_mult_cancel)
    1.10  
    1.11  lemma prod_list_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (prod_list xs) y"
    1.12 @@ -1373,7 +1373,7 @@
    1.13    also have "lcm a \<dots> = lcm a (\<Prod>A)"
    1.14      by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
    1.15    also from insert have "gcd a (\<Prod>A) = 1"
    1.16 -    by (subst gcd.commute, intro setprod_coprime) auto
    1.17 +    by (subst gcd.commute, intro prod_coprime) auto
    1.18    with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
    1.19      by (simp add: lcm_coprime)
    1.20    finally show ?case .