Division-polynomial roots from scalar multiplication

This file proves the forward division-polynomial root criterion at 5 and 7. The proof uses only the affine group law and the first few univariate division polynomials.

theorem MazurTorsion.DivisionPolynomialRootCriterion.hasDivisionPolynomialRootCriterion_five (W : WeierstrassCurve ℚ) : OddPrimeFullTorsion.HasDivisionPolynomialRootCriterion W 5

The forward fifth-division-polynomial root criterion over ℚ.

theorem MazurTorsion.DivisionPolynomialRootCriterion.hasDivisionPolynomialRootCriterion_seven (W : WeierstrassCurve ℚ) : OddPrimeFullTorsion.HasDivisionPolynomialRootCriterion W 7

The forward seventh-division-polynomial root criterion over ℚ.