Documentation

MazurTorsion.Kubert.OrderSevenIsogenyPolynomialData

Shared polynomial data for the explicit order-seven isogeny #

This file packages the source kernel cubic and the cleared Vélu abscissa as univariate polynomials. They are shared by the doubling and dual-kernel certificates.

source
noncomputable def MazurTorsion.Kubert.OrderSevenIsogenyPolynomialData.kernelPolynomial (d : ℚ) :
Polynomial ℚ

The polynomial form of the three source kernel abscissae.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MazurTorsion.Kubert.OrderSevenIsogenyPolynomialData.veluXPolynomial (d : ℚ) :
    Polynomial ℚ

    The polynomial form of the cleared explicit Vélu abscissa numerator.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem MazurTorsion.Kubert.OrderSevenIsogenyPolynomialData.kernelPolynomial_eval (d x : ℚ) :
      Polynomial.eval x (kernelPolynomial d) = orderSevenKernelPolynomial d x
      source
      @[simp]
      theorem MazurTorsion.Kubert.OrderSevenIsogenyPolynomialData.veluXPolynomial_eval (d x : ℚ) :
      Polynomial.eval x (veluXPolynomial d) = orderSevenVeluXNumerator d x