Theorem 9.2.
Assuming that:
K
a local field with
char
K
=
0
,
char
k
=
p
>
0
F
a
formal group
over
O
K
e
=
v
(
p
)
r
>
e
p
−
1
Then
log
:
F
(
π
r
O
K
)
→
≅
𝔾
^
a
(
π
r
O
K
)
is an isomorphism of groups with inverse
exp
:
𝔾
^
a
(
π
r
O
K
)
→
≅
F
(
π
r
O
K
)
.