Endomorphisms of the additive formal group without additive torsion

Over a commutative ring without additive torsion, every endomorphism of the additive formal group is multiplication by its linear coefficient. This applies to the homomorphism obtained by conjugating an integral formal-group homomorphism by integral logarithms.

References

• M. Hazewinkel, Formal Groups and Applications, I §1.

theorem TauCeti.FormalGroupHom.toPowerSeries_eq_coeff_one_smul_X {R : Type u_1} [CommRing R] [HasUniqueDiv R] (f : FormalGroupHom FormalGroup.𝔾ₐ FormalGroup.𝔾ₐ) : f.toPowerSeries = (PowerSeries.coeff 1) f.toPowerSeries • PowerSeries.X

Over a ring without additive torsion, an endomorphism of the additive formal group is multiplication by its linear coefficient.