R:(Id
), in,out:(|R|IdLnk), i,j:|R|.
Thm* ring(R;in;out)
Thm*
Thm*
x.n(x)^d(i;j)(i) = j & (k:
. k<d(i;j) 
x.n(x)^k(i) = j)f:(). (
n:. f(n)) mu(f) 
f:(). (n:. f(n)) f(mu(f)) & (i:. i<mu(f) f(i))| Theorem | Name |
| R:(Id), in,out:(|R|IdLnk), i,j:|R|.
Thm* ring(R;in;out) Thm*
Thm* x.n(x)^d(i;j)(i) = j & (k:. k<d(i;j) x.n(x)^k(i) = j) | [rdist-property] |
| cites the following: | |
| f:(). (n:. f(n)) mu(f) | [mu_wf] |
| f:(). (n:. f(n)) f(mu(f)) & (i:. i<mu(f) f(i)) | [mu-property] |