equal
deleted
inserted
replaced
427 |
427 |
428 lemma sqrt_even_pow2: |
428 lemma sqrt_even_pow2: |
429 assumes n: "even n" |
429 assumes n: "even n" |
430 shows "sqrt (2 ^ n) = 2 ^ (n div 2)" |
430 shows "sqrt (2 ^ n) = 2 ^ (n div 2)" |
431 proof - |
431 proof - |
432 from n obtain m where m: "n = 2 * m" |
432 from n obtain m where m: "n = 2 * m" .. |
433 unfolding even_mult_two_ex .. |
|
434 from m have "sqrt (2 ^ n) = sqrt ((2 ^ m)\<^sup>2)" |
433 from m have "sqrt (2 ^ n) = sqrt ((2 ^ m)\<^sup>2)" |
435 by (simp only: power_mult[symmetric] mult.commute) |
434 by (simp only: power_mult[symmetric] mult.commute) |
436 then show ?thesis |
435 then show ?thesis |
437 using m by simp |
436 using m by simp |
438 qed |
437 qed |