Torsion-freeness of the formal group over Qp for odd p (source code)

= Torsion-freeness of the formal group over Qp for odd p
{title2=$\widehat E(p\mathbb Z_p)\text{ is torsion-free}$}

For odd $p$, a one-dimensional <formal group law> over $\mathbb Z_p$ has a <formal logarithm> $\log_F(T)=T+\sum_{j\geq2}c_jT^j/j$ with $c_j\in\mathbb Z_p$. This follows by integrating its integral invariant differential. For $t\in p\mathbb Z_p\setminus\{0\}$, $v_p(c_jt^j/j)>v_p(t)$ for $j\geq2$. Hence the series converges and $v_p(\log_F(t))=v_p(t)$, so its kernel is zero. As it is a homomorphism into a characteristic-zero additive group, there is no nonzero torsion. In particular, at an odd <prime> of <good reduction> over $\mathbb Q$, reduction injects the whole rational <torsion subgroup>, including its $p$-primary part.