equal
deleted
inserted
replaced
58 |
58 |
59 lemma hypreal_sqrt_mult_distrib: |
59 lemma hypreal_sqrt_mult_distrib: |
60 "!!x y. [|0 < x; 0 <y |] ==> |
60 "!!x y. [|0 < x; 0 <y |] ==> |
61 ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)" |
61 ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)" |
62 apply transfer |
62 apply transfer |
63 apply (auto intro: real_sqrt_mult_distrib) |
63 apply (auto intro: real_sqrt_mult) |
64 done |
64 done |
65 |
65 |
66 lemma hypreal_sqrt_mult_distrib2: |
66 lemma hypreal_sqrt_mult_distrib2: |
67 "[|0\<le>x; 0\<le>y |] ==> |
67 "[|0\<le>x; 0\<le>y |] ==> |
68 ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)" |
68 ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)" |