equal
deleted
inserted
replaced
379 apply (simp add: star_inverse_def Ifun_of_def star_of_def Ifun_star_n) |
379 apply (simp add: star_inverse_def Ifun_of_def star_of_def Ifun_star_n) |
380 apply (rule_tac f=star_n in arg_cong) |
380 apply (rule_tac f=star_n in arg_cong) |
381 apply (rule ext) |
381 apply (rule ext) |
382 apply simp |
382 apply simp |
383 done |
383 done |
|
384 |
|
385 lemma hypreal_inverse2 [unfolded star_n_def]: |
|
386 "inverse (star_n X) = star_n (%n. inverse(X n))" |
|
387 by (simp add: star_inverse_def Ifun_of_def star_of_def Ifun_star_n) |
384 |
388 |
385 lemma hypreal_mult_inverse: |
389 lemma hypreal_mult_inverse: |
386 "x \<noteq> 0 ==> x*inverse(x) = (1::hypreal)" |
390 "x \<noteq> 0 ==> x*inverse(x) = (1::hypreal)" |
387 by (rule right_inverse) |
391 by (rule right_inverse) |
388 |
392 |