src/HOL/NthRoot.thy
changeset 66815 93c6632ddf44
parent 65552 f533820e7248
child 67685 bdff8bf0a75b
     1.1 --- a/src/HOL/NthRoot.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/NthRoot.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -218,7 +218,7 @@
     1.4  
     1.5  lemma real_root_inverse: "root n (inverse x) = inverse (root n x)"
     1.6    by (auto split: split_root elim!: sgn_power_injE
     1.7 -      simp: inverse_sgn power_inverse)
     1.8 +      simp: power_inverse)
     1.9  
    1.10  lemma real_root_divide: "root n (x / y) = root n x / root n y"
    1.11    by (simp add: divide_inverse real_root_mult real_root_inverse)
    1.12 @@ -715,7 +715,7 @@
    1.13      have "x n \<le> sqrt (2 / real n)" if "2 < n" for n :: nat
    1.14      proof -
    1.15        have "1 + (real (n - 1) * n) / 2 * (x n)\<^sup>2 = 1 + of_nat (n choose 2) * (x n)\<^sup>2"
    1.16 -        by (auto simp add: choose_two of_nat_div mod_eq_0_iff_dvd)
    1.17 +        by (auto simp add: choose_two field_char_0_class.of_nat_div mod_eq_0_iff_dvd)
    1.18        also have "\<dots> \<le> (\<Sum>k\<in>{0, 2}. of_nat (n choose k) * x n^k)"
    1.19          by (simp add: x_def)
    1.20        also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"