k:
, f:(k inj
k). 
i:
. f{
i} = Id 
k
kk:, f:(k inj k). i:. u:k. f{i}(u) = u| Rank | Theorem | Name |
| 7 | k:, f:(k inj k). i:. f{i} = Id kk | [iter_perm_cycles_uniform2] |
| cites the following: | ||
| 6 | k:, f:(k inj k). i:. u:k. f{i}(u) = u | [iter_perm_cycles_uniform] |