src/HOL/GCD.thy
changeset 64240 eabf80376aab
parent 63924 f91766530e13
child 64242 93c6f0da5c70
     1.1 --- a/src/HOL/GCD.thy	Sun Oct 16 09:31:03 2016 +0200
     1.2 +++ b/src/HOL/GCD.thy	Sun Oct 16 09:31:04 2016 +0200
     1.3 @@ -356,7 +356,7 @@
     1.4    then have "gcd a b * lcm a b div lcm a b = normalize (a * b) div lcm a b"
     1.5      by (simp_all add: normalize_mult)
     1.6    with \<open>lcm a b \<noteq> 0\<close> show ?thesis
     1.7 -    using nonzero_mult_divide_cancel_right [of "lcm a b" "gcd a b"] by simp
     1.8 +    using nonzero_mult_div_cancel_right [of "lcm a b" "gcd a b"] by simp
     1.9  qed
    1.10  
    1.11  lemma lcm_1_left [simp]: "lcm 1 a = normalize a"