theorem Schoof.addOrderOf_eq_prime_of_torsion {G : Type u_1} [AddGroup G] {P : G} {ℓ : ℕ} (hℓ : Nat.Prime ℓ) (hP : ↑ℓ • P = 0) (hne : P ≠ 0) : addOrderOf P = ℓ

If P is a nonzero element of an additive group annihilated by a prime ℓ, then the additive order of P equals ℓ. Used in Schoof's algorithm to control the order of ℓ-torsion points on an elliptic curve.

theorem Schoof.zmod_eq_of_dvd_sub {c t : ℤ} {ℓ : ℕ} (hdvd : ↑ℓ ∣ c - t) : ↑c = ↑t

If ℓ divides c - t in ℤ, then c and t represent the same residue class in ZMod ℓ. A small bridging lemma used to read off the trace of Frobenius modulo ℓ from an integer congruence.

theorem Schoof.frobenius_trace_mod_ell {F : Type u} [Field F] [DecidableEq F] {W : WeierstrassCurve.Affine F} (π : W.Point →+ W.Point) (t q : ℤ) (ℓ : ℕ) (hℓ : Nat.Prime ℓ) (char_eq : ∀ (P : W.Point), ↑ℓ • P = 0 → π (π P) - t • π P + q • P = 0) (frob_torsion : ∀ (P : W.Point), ↑ℓ • P = 0 → ↑ℓ • π P = 0) (frob_nonzero : ∀ (P : W.Point), ↑ℓ • P = 0 → P ≠ 0 → π P ≠ 0) {P : W.Point} (hP_torsion : ↑ℓ • P = 0) (hP_ne : P ≠ 0) {c : ℤ} (hc : π (π P) - c • π P + q • P = 0) : ↑c = ↑t

Lemma 8.2: let E/𝔽_q have Frobenius π, let ℓ be a prime with ℓ ∤ q, and let P ∈ E[ℓ] be nonzero. If for some integer c the equation π_ℓ²(P) - c · π_ℓ(P) + q_ℓ · P = 0 holds, then c ≡ tr π (mod ℓ). This is the core congruence underlying Schoof's algorithm: any integer c solving the characteristic equation on a single nonzero ℓ-torsion point must agree with the trace of Frobenius modulo ℓ.