x:
. 1
x = 1f:(A
AA), u:A.
Thm* is_ident(A; f; u)
Thm*
Thm* (
a,b:, e:({a..b
}A).
Thm* ((
i:{a..b}. e(i) = u) (Iter(f;u) i:{a..b}. e(i)) = u); (
x,y. x
y); 1)| Rank | Theorem | Name |
| 3 | x:. 1x = 1 | [one_exponentiation] |
| cites the following: | ||
| 2 | f:(AAA), u:A.
Thm* is_ident(A; f; u) Thm*
Thm* ( a,b:, e:({a..b}A).
Thm* (( i:{a..b}. e(i) = u) (Iter(f;u) i:{a..b}. e(i)) = u) | [iter_via_intseg_all_units] |
| 0 | ; (x,y. xy); 1) | [intmul_ident_one] |