src/HOL/Computational_Algebra/Nth_Powers.thy
changeset 67051 e7e54a0b9197
parent 66276 acc3b7dd0b21
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Computational_Algebra/Nth_Powers.thy	Sat Nov 11 18:33:35 2017 +0000
     1.2 +++ b/src/HOL/Computational_Algebra/Nth_Powers.thy	Sat Nov 11 18:41:08 2017 +0000
     1.3 @@ -111,9 +111,10 @@
     1.4      ultimately show "n dvd multiplicity p a"
     1.5        by (auto simp: not_dvd_imp_multiplicity_0)
     1.6    qed
     1.7 -  from A[of a b] assms show "is_nth_power n a" by (cases "n = 0") simp_all
     1.8 -  from A[of b a] assms show "is_nth_power n b" 
     1.9 -    by (cases "n = 0") (simp_all add: gcd.commute mult.commute)
    1.10 +  from A [of a b] assms show "is_nth_power n a"
    1.11 +    by (cases "n = 0") simp_all
    1.12 +  from A [of b a] assms show "is_nth_power n b"
    1.13 +    by (cases "n = 0") (simp_all add: ac_simps)
    1.14  qed
    1.15      
    1.16  lemma is_nth_power_mult_coprime_nat_iff: