equal
deleted
inserted
replaced
163 thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp:Let_def) |
163 thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp:Let_def) |
164 qed |
164 qed |
165 qed |
165 qed |
166 |
166 |
167 lemma Rats_eq_range_nat_to_rat_surj: "\<rat> = range nat_to_rat_surj" |
167 lemma Rats_eq_range_nat_to_rat_surj: "\<rat> = range nat_to_rat_surj" |
168 by (simp add: Rats_def surj_nat_to_rat_surj surj_range) |
168 by (simp add: Rats_def surj_nat_to_rat_surj) |
169 |
169 |
170 context field_char_0 |
170 context field_char_0 |
171 begin |
171 begin |
172 |
172 |
173 lemma Rats_eq_range_of_rat_o_nat_to_rat_surj: |
173 lemma Rats_eq_range_of_rat_o_nat_to_rat_surj: |