equal
deleted
inserted
replaced
311 "y \<noteq> 0 \<Longrightarrow> of_real (x / y) = |
311 "y \<noteq> 0 \<Longrightarrow> of_real (x / y) = |
312 (of_real x / of_real y :: 'a::real_field)" |
312 (of_real x / of_real y :: 'a::real_field)" |
313 by (simp add: divide_inverse nonzero_of_real_inverse) |
313 by (simp add: divide_inverse nonzero_of_real_inverse) |
314 |
314 |
315 lemma of_real_divide [simp]: |
315 lemma of_real_divide [simp]: |
316 "of_real (x / y) = |
316 "of_real (x / y) = (of_real x / of_real y :: 'a::real_div_algebra)" |
317 (of_real x / of_real y :: 'a::{real_field, field})" |
|
318 by (simp add: divide_inverse) |
317 by (simp add: divide_inverse) |
319 |
318 |
320 lemma of_real_power [simp]: |
319 lemma of_real_power [simp]: |
321 "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1}) ^ n" |
320 "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1}) ^ n" |
322 by (induct n) simp_all |
321 by (induct n) simp_all |