The generic point of an elliptic curve has infinite order

For an elliptic curve over a field, every nonzero integer multiple of its generic point is nonzero. Consequently, distinct integers give distinct multiples of the generic point.

Main results

• WeierstrassCurve.Affine.zsmul_genericPoint_ne_zero: every nonzero multiple of the generic point is nonzero.
• WeierstrassCurve.Affine.zsmul_genericPoint_injective: multiplication of the generic point by an integer is injective.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.4.

theorem WeierstrassCurve.Affine.zsmul_genericPoint_ne_zero {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : n ≠ 0) : n • W.genericPoint ≠ 0

The generic point of an elliptic curve is not torsion: every nonzero integer multiple is nonzero.

theorem WeierstrassCurve.Affine.zsmul_genericPoint_injective {F : Type u_1} [Field F] (W : Affine F) [WeierstrassCurve.IsElliptic W] : Function.Injective fun (n : ℤ) => n • W.genericPoint

The multiples of the generic point are pairwise distinct, the generic point having infinite order.