@[instance_reducible]

noncomputable instance Hex.ECPP.pointFintype {F : Type u_1} [CommRing F] [Fintype F] (W : WeierstrassCurve.Affine F) : Fintype W.Point

Over a finite ring, the nonsingular affine points and infinity form a finite type, via Mathlib's nonsingular-point equivalence.

Equations

• Hex.ECPP.pointFintype W = Fintype.ofEquiv (WithZero { xy : F × F // W.Nonsingular xy.1 xy.2 }) W.nonsingularPointEquiv.symm

theorem Hex.ECPP.hasse_sq {F : Type u_1} [Field F] [Fintype F] (W : WeierstrassCurve F) [WeierstrassCurve.IsElliptic W.toAffine] : (↑(Fintype.card F) + 1 - ↑(Fintype.card W.toAffine.Point)) ^ 2 ≤ 4 * ↑(Fintype.card F)

Hasse's bound on the number of points of an elliptic curve over a finite field, written as an exact integer inequality. If N is the point count and r the field size, (r + 1 - N)² ≤ 4*r. The proof uses TauCeti's WeierstrassCurve.hasse_bound, whose dependencies contain only the standard Lean axioms.