equal
deleted
inserted
replaced
16 The set of rational numbers, including the key representation |
16 The set of rational numbers, including the key representation |
17 theorem. |
17 theorem. |
18 *} |
18 *} |
19 |
19 |
20 definition |
20 definition |
21 rationals ("\<rat>") |
21 rationals ("\<rat>") where |
22 "\<rat> = {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}" |
22 "\<rat> = {x. \<exists>m n. n \<noteq> 0 \<and> \<bar>x\<bar> = real (m::nat) / real (n::nat)}" |
23 |
23 |
24 theorem rationals_rep [elim?]: |
24 theorem rationals_rep [elim?]: |
25 assumes "x \<in> \<rat>" |
25 assumes "x \<in> \<rat>" |
26 obtains m n where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd (m, n) = 1" |
26 obtains m n where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd (m, n) = 1" |