'a,'b:S, P:('b
), rep:('a'b), abs:('b'a), a:'a, r:'b.
Thm* iso_pair('a;'b;P;rep;abs)
rep(a) = r a = abs(r)
;;is_num_rep;rep_num;abs_num)| Rank | Theorem | Name |
| 3 | [hzero_def] | |
| cites the following: | ||
| 2 | 'a,'b:S, P:('b), rep:('a'b), abs:('b'a), a:'a, r:'b.
Thm* iso_pair('a;'b;P;rep;abs) rep(a) = r a = abs(r) | [iso_pair_rep_to_abs] |
| 0 | ;;is_num_rep;rep_num;abs_num) | [num_iso] |