Documentation

Mathlib.AlgebraicGeometry.EllipticCurve.Projective

Projective coordinates for Weierstrass curves #

This file defines the type of points on a Weierstrass curve as a tuple, consisting of an equivalence class of triples up to scaling by a unit, satisfying a Weierstrass equation with a nonsingular condition.

Mathematical background #

Let W be a Weierstrass curve over a field F. A point on the projective plane is an equivalence class of triples $[x:y:z]$ with coordinates in F such that $(x, y, z) \sim (x', y', z')$ precisely if there is some unit u of F such that $(x, y, z) = (ux', uy', uz')$, with an extra condition that $(x, y, z) \ne (0, 0, 0)$. As described in Mathlib.AlgebraicGeometry.EllipticCurve.Affine, a rational point is a point on the projective plane satisfying a homogeneous Weierstrass equation, and being nonsingular means the partial derivatives $W_X(X, Y, Z)$, $W_Y(X, Y, Z)$, and $W_Z(X, Y, Z)$ do not vanish simultaneously. Note that the vanishing of the Weierstrass equation and its partial derivatives are independent of the representative for $[x:y:z]$, and the nonsingularity condition already implies that $(x, y, z) \ne (0, 0, 0)$, so a nonsingular rational point on W can simply be given by a tuple consisting of $[x:y:z]$ and the nonsingular condition on any representative.

As in Mathlib.AlgebraicGeometry.EllipticCurve.Affine, the set of nonsingular rational points forms an abelian group under the same secant-and-tangent process, but the polynomials involved are homogeneous, and any instances of division become multiplication in the $Z$-coordinate.

Main definitions #

Main statements #

Implementation notes #

A point representative is implemented as a term P of type Fin 3 → R, which allows for the vector notation ![x, y, z]. However, P is not definitionally equivalent to the expanded vector ![P x, P y, P z], so the lemmas fin3_def and fin3_def_ext can be used to convert between the two forms. The equivalence of two point representatives P and Q is implemented as an equivalence of orbits of the action of , or equivalently that there is some unit u of R such that P = u • Q. However, u • Q is not definitionally equal to ![u * Q x, u * Q y, u * Q z], so the lemmas smul_fin3 and smul_fin3_ext can be used to convert between the two forms.

References #

J Silverman, The Arithmetic of Elliptic Curves

Tags #

elliptic curve, rational point, projective coordinates

Weierstrass curves #

@[reducible, inline]

An abbreviation for a Weierstrass curve in projective coordinates.

Equations
Instances For
    @[reducible, inline]

    The coercion to a Weierstrass curve in projective coordinates.

    Equations
    • W.toProjective = W
    Instances For

      Projective coordinates #

      theorem WeierstrassCurve.Projective.fin3_def {R : Type u} (P : Fin 3R) :
      ![P 0, P 1, P 2] = P
      theorem WeierstrassCurve.Projective.fin3_def_ext {R : Type u} (X : R) (Y : R) (Z : R) :
      ![X, Y, Z] 0 = X ![X, Y, Z] 1 = Y ![X, Y, Z] 2 = Z
      theorem WeierstrassCurve.Projective.comp_fin3 {R : Type u} {S : Type v} (f : RS) (X : R) (Y : R) (Z : R) :
      f ![X, Y, Z] = ![f X, f Y, f Z]
      theorem WeierstrassCurve.Projective.smul_fin3 {R : Type u} [CommRing R] (P : Fin 3R) (u : R) :
      u P = ![u * P 0, u * P 1, u * P 2]
      theorem WeierstrassCurve.Projective.smul_fin3_ext {R : Type u} [CommRing R] (P : Fin 3R) (u : R) :
      (u P) 0 = u * P 0 (u P) 1 = u * P 1 (u P) 2 = u * P 2

      The equivalence setoid for a point representative.

      Equations
      Instances For
        @[reducible, inline]

        The equivalence class of a point representative.

        Equations
        Instances For
          theorem WeierstrassCurve.Projective.smul_equiv {R : Type u} [CommRing R] (P : Fin 3R) {u : R} (hu : IsUnit u) :
          u P P
          @[simp]
          theorem WeierstrassCurve.Projective.smul_eq {R : Type u} [CommRing R] (P : Fin 3R) {u : R} (hu : IsUnit u) :
          u P = P
          @[reducible, inline]

          The coercion to a Weierstrass curve in affine coordinates.

          Equations
          • W'.toAffine = W'
          Instances For
            theorem WeierstrassCurve.Projective.equiv_iff_eq_of_Z_eq' {R : Type u} [CommRing R] {P : Fin 3R} {Q : Fin 3R} (hz : P 2 = Q 2) (mem : Q 2 nonZeroDivisors R) :
            P Q P = Q
            theorem WeierstrassCurve.Projective.equiv_iff_eq_of_Z_eq {R : Type u} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hz : P 2 = Q 2) (hQz : Q 2 0) :
            P Q P = Q
            theorem WeierstrassCurve.Projective.Z_eq_zero_of_equiv {R : Type u} [CommRing R] {P : Fin 3R} {Q : Fin 3R} (h : P Q) :
            P 2 = 0 Q 2 = 0
            theorem WeierstrassCurve.Projective.X_eq_of_equiv {R : Type u} [CommRing R] {P : Fin 3R} {Q : Fin 3R} (h : P Q) :
            P 0 * Q 2 = Q 0 * P 2
            theorem WeierstrassCurve.Projective.Y_eq_of_equiv {R : Type u} [CommRing R] {P : Fin 3R} {Q : Fin 3R} (h : P Q) :
            P 1 * Q 2 = Q 1 * P 2
            theorem WeierstrassCurve.Projective.not_equiv_of_Z_eq_zero_left {R : Type u} [CommRing R] {P : Fin 3R} {Q : Fin 3R} (hPz : P 2 = 0) (hQz : Q 2 0) :
            ¬P Q
            theorem WeierstrassCurve.Projective.not_equiv_of_Z_eq_zero_right {R : Type u} [CommRing R] {P : Fin 3R} {Q : Fin 3R} (hPz : P 2 0) (hQz : Q 2 = 0) :
            ¬P Q
            theorem WeierstrassCurve.Projective.not_equiv_of_X_ne {R : Type u} [CommRing R] {P : Fin 3R} {Q : Fin 3R} (hx : P 0 * Q 2 Q 0 * P 2) :
            ¬P Q
            theorem WeierstrassCurve.Projective.not_equiv_of_Y_ne {R : Type u} [CommRing R] {P : Fin 3R} {Q : Fin 3R} (hy : P 1 * Q 2 Q 1 * P 2) :
            ¬P Q
            theorem WeierstrassCurve.Projective.equiv_of_X_eq_of_Y_eq {F : Type v} [Field F] {P : Fin 3F} {Q : Fin 3F} (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 = Q 1 * P 2) :
            P Q
            theorem WeierstrassCurve.Projective.equiv_some_of_Z_ne_zero {F : Type v} [Field F] {P : Fin 3F} (hPz : P 2 0) :
            P ![P 0 / P 2, P 1 / P 2, 1]
            theorem WeierstrassCurve.Projective.X_eq_iff {F : Type v} [Field F] {P : Fin 3F} {Q : Fin 3F} (hPz : P 2 0) (hQz : Q 2 0) :
            P 0 * Q 2 = Q 0 * P 2 P 0 / P 2 = Q 0 / Q 2
            theorem WeierstrassCurve.Projective.Y_eq_iff {F : Type v} [Field F] {P : Fin 3F} {Q : Fin 3F} (hPz : P 2 0) (hQz : Q 2 0) :
            P 1 * Q 2 = Q 1 * P 2 P 1 / P 2 = Q 1 / Q 2

            Weierstrass equations #

            The polynomial $W(X, Y, Z) := Y^2Z + a_1XYZ + a_3YZ^2 - (X^3 + a_2X^2Z + a_4XZ^2 + a_6Z^3)$ associated to a Weierstrass curve W' over R. This is represented as a term of type MvPolynomial (Fin 3) R, where X 0, X 1, and X 2 represent $X$, $Y$, and $Z$ respectively.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem WeierstrassCurve.Projective.eval_polynomial {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
              (MvPolynomial.eval P) W'.polynomial = P 1 ^ 2 * P 2 + W'.a₁ * P 0 * P 1 * P 2 + W'.a₃ * P 1 * P 2 ^ 2 - (P 0 ^ 3 + W'.a₂ * P 0 ^ 2 * P 2 + W'.a₄ * P 0 * P 2 ^ 2 + W'.a₆ * P 2 ^ 3)
              theorem WeierstrassCurve.Projective.eval_polynomial_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hPz : P 2 0) :
              (MvPolynomial.eval P) W.polynomial / P 2 ^ 3 = Polynomial.evalEval (P 0 / P 2) (P 1 / P 2) W.toAffine.polynomial

              The proposition that a point representative $(x, y, z)$ lies in W'. In other words, $W(x, y, z) = 0$.

              Equations
              Instances For
                theorem WeierstrassCurve.Projective.equation_iff {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                W'.Equation P P 1 ^ 2 * P 2 + W'.a₁ * P 0 * P 1 * P 2 + W'.a₃ * P 1 * P 2 ^ 2 - (P 0 ^ 3 + W'.a₂ * P 0 ^ 2 * P 2 + W'.a₄ * P 0 * P 2 ^ 2 + W'.a₆ * P 2 ^ 3) = 0
                theorem WeierstrassCurve.Projective.equation_smul {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) {u : R} (hu : IsUnit u) :
                W'.Equation (u P) W'.Equation P
                theorem WeierstrassCurve.Projective.equation_of_equiv {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3R} {Q : Fin 3R} (h : P Q) :
                W'.Equation P W'.Equation Q
                theorem WeierstrassCurve.Projective.equation_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3R} (hPz : P 2 = 0) :
                W'.Equation P P 0 ^ 3 = 0
                theorem WeierstrassCurve.Projective.equation_some {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (X : R) (Y : R) :
                W'.Equation ![X, Y, 1] W'.toAffine.Equation X Y
                theorem WeierstrassCurve.Projective.equation_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hPz : P 2 0) :
                W.Equation P W.toAffine.Equation (P 0 / P 2) (P 1 / P 2)
                theorem WeierstrassCurve.Projective.X_eq_zero_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} (hP : W'.Equation P) (hPz : P 2 = 0) :
                P 0 = 0

                Nonsingular Weierstrass equations #

                The partial derivative $W_X(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $X$.

                Equations
                Instances For
                  theorem WeierstrassCurve.Projective.polynomialX_eq {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] :
                  W'.polynomialX = MvPolynomial.C W'.a₁ * MvPolynomial.X 1 * MvPolynomial.X 2 - (MvPolynomial.C 3 * MvPolynomial.X 0 ^ 2 + MvPolynomial.C (2 * W'.a₂) * MvPolynomial.X 0 * MvPolynomial.X 2 + MvPolynomial.C W'.a₄ * MvPolynomial.X 2 ^ 2)
                  theorem WeierstrassCurve.Projective.eval_polynomialX {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                  (MvPolynomial.eval P) W'.polynomialX = W'.a₁ * P 1 * P 2 - (3 * P 0 ^ 2 + 2 * W'.a₂ * P 0 * P 2 + W'.a₄ * P 2 ^ 2)
                  theorem WeierstrassCurve.Projective.eval_polynomialX_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hPz : P 2 0) :
                  (MvPolynomial.eval P) W.polynomialX / P 2 ^ 2 = Polynomial.evalEval (P 0 / P 2) (P 1 / P 2) W.toAffine.polynomialX

                  The partial derivative $W_Y(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $Y$.

                  Equations
                  Instances For
                    theorem WeierstrassCurve.Projective.polynomialY_eq {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] :
                    W'.polynomialY = MvPolynomial.C 2 * MvPolynomial.X 1 * MvPolynomial.X 2 + MvPolynomial.C W'.a₁ * MvPolynomial.X 0 * MvPolynomial.X 2 + MvPolynomial.C W'.a₃ * MvPolynomial.X 2 ^ 2
                    theorem WeierstrassCurve.Projective.eval_polynomialY {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                    (MvPolynomial.eval P) W'.polynomialY = 2 * P 1 * P 2 + W'.a₁ * P 0 * P 2 + W'.a₃ * P 2 ^ 2
                    theorem WeierstrassCurve.Projective.eval_polynomialY_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hPz : P 2 0) :
                    (MvPolynomial.eval P) W.polynomialY / P 2 ^ 2 = Polynomial.evalEval (P 0 / P 2) (P 1 / P 2) W.toAffine.polynomialY

                    The partial derivative $W_Z(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $Z$.

                    Equations
                    Instances For
                      theorem WeierstrassCurve.Projective.polynomialZ_eq {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] :
                      W'.polynomialZ = MvPolynomial.X 1 ^ 2 + MvPolynomial.C W'.a₁ * MvPolynomial.X 0 * MvPolynomial.X 1 + MvPolynomial.C (2 * W'.a₃) * MvPolynomial.X 1 * MvPolynomial.X 2 - (MvPolynomial.C W'.a₂ * MvPolynomial.X 0 ^ 2 + MvPolynomial.C (2 * W'.a₄) * MvPolynomial.X 0 * MvPolynomial.X 2 + MvPolynomial.C (3 * W'.a₆) * MvPolynomial.X 2 ^ 2)
                      theorem WeierstrassCurve.Projective.eval_polynomialZ {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                      (MvPolynomial.eval P) W'.polynomialZ = P 1 ^ 2 + W'.a₁ * P 0 * P 1 + 2 * W'.a₃ * P 1 * P 2 - (W'.a₂ * P 0 ^ 2 + 2 * W'.a₄ * P 0 * P 2 + 3 * W'.a₆ * P 2 ^ 2)
                      theorem WeierstrassCurve.Projective.polynomial_relation {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                      3 * (MvPolynomial.eval P) W'.polynomial = P 0 * (MvPolynomial.eval P) W'.polynomialX + P 1 * (MvPolynomial.eval P) W'.polynomialY + P 2 * (MvPolynomial.eval P) W'.polynomialZ

                      Euler's homogeneous function theorem.

                      The proposition that a point representative $(x, y, z)$ in W' is nonsingular. In other words, either $W_X(x, y, z) \ne 0$, $W_Y(x, y, z) \ne 0$, or $W_Z(x, y, z) \ne 0$.

                      Note that this definition is only mathematically accurate for fields.

                      Equations
                      Instances For
                        theorem WeierstrassCurve.Projective.nonsingular_iff {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                        W'.Nonsingular P W'.Equation P (W'.a₁ * P 1 * P 2 - (3 * P 0 ^ 2 + 2 * W'.a₂ * P 0 * P 2 + W'.a₄ * P 2 ^ 2) 0 2 * P 1 * P 2 + W'.a₁ * P 0 * P 2 + W'.a₃ * P 2 ^ 2 0 P 1 ^ 2 + W'.a₁ * P 0 * P 1 + 2 * W'.a₃ * P 1 * P 2 - (W'.a₂ * P 0 ^ 2 + 2 * W'.a₄ * P 0 * P 2 + 3 * W'.a₆ * P 2 ^ 2) 0)
                        theorem WeierstrassCurve.Projective.nonsingular_smul {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) {u : R} (hu : IsUnit u) :
                        W'.Nonsingular (u P) W'.Nonsingular P
                        theorem WeierstrassCurve.Projective.nonsingular_of_equiv {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3R} {Q : Fin 3R} (h : P Q) :
                        W'.Nonsingular P W'.Nonsingular Q
                        theorem WeierstrassCurve.Projective.nonsingular_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3R} (hPz : P 2 = 0) :
                        W'.Nonsingular P W'.Equation P (3 * P 0 ^ 2 0 P 1 ^ 2 + W'.a₁ * P 0 * P 1 - W'.a₂ * P 0 ^ 2 0)
                        theorem WeierstrassCurve.Projective.nonsingular_some {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (X : R) (Y : R) :
                        W'.Nonsingular ![X, Y, 1] W'.toAffine.Nonsingular X Y
                        theorem WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hPz : P 2 0) :
                        W.Nonsingular P W.toAffine.Nonsingular (P 0 / P 2) (P 1 / P 2)
                        theorem WeierstrassCurve.Projective.nonsingular_iff_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hPz : P 2 0) :
                        W.Nonsingular P W.Equation P ((MvPolynomial.eval P) W.polynomialX 0 (MvPolynomial.eval P) W.polynomialY 0)
                        theorem WeierstrassCurve.Projective.Y_ne_zero_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} (hP : W'.Nonsingular P) (hPz : P 2 = 0) :
                        P 1 0
                        theorem WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hP : W.Nonsingular P) (hPz : P 2 = 0) :
                        IsUnit (P 1)
                        theorem WeierstrassCurve.Projective.equiv_of_Z_eq_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) (hPz : P 2 = 0) (hQz : Q 2 = 0) :
                        P Q
                        theorem WeierstrassCurve.Projective.equiv_zero_of_Z_eq_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hP : W.Nonsingular P) (hPz : P 2 = 0) :
                        P ![0, 1, 0]

                        The proposition that a point class on W' is nonsingular. If P is a point representative, then W.NonsingularLift ⟦P⟧ is definitionally equivalent to W.Nonsingular P.

                        Equations
                        Instances For
                          theorem WeierstrassCurve.Projective.nonsingularLift_iff {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                          W'.NonsingularLift P W'.Nonsingular P
                          theorem WeierstrassCurve.Projective.nonsingularLift_zero {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [Nontrivial R] :
                          W'.NonsingularLift ![0, 1, 0]
                          theorem WeierstrassCurve.Projective.nonsingularLift_some {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (X : R) (Y : R) :
                          W'.NonsingularLift ![X, Y, 1] W'.toAffine.Nonsingular X Y
                          @[deprecated WeierstrassCurve.Projective.equation_smul]
                          theorem WeierstrassCurve.Projective.equation_smul_iff {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) {u : R} (hu : IsUnit u) :
                          W'.Equation (u P) W'.Equation P

                          Alias of WeierstrassCurve.Projective.equation_smul.

                          @[deprecated WeierstrassCurve.Projective.nonsingularLift_zero]
                          theorem WeierstrassCurve.Projective.nonsingularLift_zero' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [Nontrivial R] :
                          W'.NonsingularLift ![0, 1, 0]

                          Alias of WeierstrassCurve.Projective.nonsingularLift_zero.

                          @[deprecated WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero]
                          theorem WeierstrassCurve.Projective.nonsingular_affine_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hPz : P 2 0) :
                          W.Nonsingular P W.toAffine.Nonsingular (P 0 / P 2) (P 1 / P 2)

                          Alias of WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero.

                          @[deprecated WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero]
                          theorem WeierstrassCurve.Projective.nonsingular_iff_affine_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hPz : P 2 0) :
                          W.Nonsingular P W.toAffine.Nonsingular (P 0 / P 2) (P 1 / P 2)

                          Alias of WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero.

                          @[deprecated WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero]
                          theorem WeierstrassCurve.Projective.nonsingular_of_affine_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hPz : P 2 0) :
                          W.Nonsingular P W.toAffine.Nonsingular (P 0 / P 2) (P 1 / P 2)

                          Alias of WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero.

                          @[deprecated WeierstrassCurve.Projective.nonsingular_smul]
                          theorem WeierstrassCurve.Projective.nonsingular_smul_iff {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) {u : R} (hu : IsUnit u) :
                          W'.Nonsingular (u P) W'.Nonsingular P

                          Alias of WeierstrassCurve.Projective.nonsingular_smul.

                          @[deprecated WeierstrassCurve.Projective.nonsingular_zero]
                          theorem WeierstrassCurve.Projective.nonsingular_zero' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [Nontrivial R] :
                          W'.Nonsingular ![0, 1, 0]

                          Alias of WeierstrassCurve.Projective.nonsingular_zero.

                          Negation formulae #

                          The $Y$-coordinate of a representative of -P for a point P.

                          Equations
                          • W'.negY P = -P 1 - W'.a₁ * P 0 - W'.a₃ * P 2
                          Instances For
                            theorem WeierstrassCurve.Projective.negY_eq {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (X : R) (Y : R) (Z : R) :
                            W'.negY ![X, Y, Z] = -Y - W'.a₁ * X - W'.a₃ * Z
                            theorem WeierstrassCurve.Projective.negY_smul {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) (u : R) :
                            W'.negY (u P) = u * W'.negY P
                            theorem WeierstrassCurve.Projective.negY_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} (hP : W'.Equation P) (hPz : P 2 = 0) :
                            W'.negY P = -P 1
                            theorem WeierstrassCurve.Projective.negY_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hPz : P 2 0) :
                            W.negY P / P 2 = W.toAffine.negY (P 0 / P 2) (P 1 / P 2)
                            theorem WeierstrassCurve.Projective.Y_sub_Y_mul_Y_sub_negY {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hx : P 0 * Q 2 = Q 0 * P 2) :
                            P 2 * Q 2 * (P 1 * Q 2 - Q 1 * P 2) * (P 1 * Q 2 - W'.negY Q * P 2) = 0
                            theorem WeierstrassCurve.Projective.Y_eq_of_Y_ne {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 Q 1 * P 2) :
                            P 1 * Q 2 = W'.negY Q * P 2
                            theorem WeierstrassCurve.Projective.Y_eq_of_Y_ne' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 W'.negY Q * P 2) :
                            P 1 * Q 2 = Q 1 * P 2
                            theorem WeierstrassCurve.Projective.Y_eq_iff' {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hPz : P 2 0) (hQz : Q 2 0) :
                            P 1 * Q 2 = W.negY Q * P 2 P 1 / P 2 = W.toAffine.negY (Q 0 / Q 2) (Q 1 / Q 2)
                            theorem WeierstrassCurve.Projective.Y_sub_Y_add_Y_sub_negY {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3R} {Q : Fin 3R} (hx : P 0 * Q 2 = Q 0 * P 2) :
                            P 1 * Q 2 - Q 1 * P 2 + (P 1 * Q 2 - W'.negY Q * P 2) = (P 1 - W'.negY P) * Q 2
                            theorem WeierstrassCurve.Projective.Y_ne_negY_of_Y_ne {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 Q 1 * P 2) :
                            P 1 W'.negY P
                            theorem WeierstrassCurve.Projective.Y_ne_negY_of_Y_ne' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 W'.negY Q * P 2) :
                            P 1 W'.negY P
                            theorem WeierstrassCurve.Projective.Y_eq_negY_of_Y_eq {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 = Q 1 * P 2) (hy' : P 1 * Q 2 = W'.negY Q * P 2) :
                            P 1 = W'.negY P
                            theorem WeierstrassCurve.Projective.nonsingular_iff_of_Y_eq_negY {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hPz : P 2 0) (hy : P 1 = W.negY P) :
                            W.Nonsingular P W.Equation P (MvPolynomial.eval P) W.polynomialX 0

                            Doubling formulae #

                            noncomputable def WeierstrassCurve.Projective.dblU {F : Type v} [Field F] (W : WeierstrassCurve.Projective F) (P : Fin 3F) :
                            F

                            The unit associated to the doubling of a 2-torsion point P. More specifically, the unit u such that W.add P P = u • ![0, 1, 0] where P = W.neg P.

                            Equations
                            Instances For
                              theorem WeierstrassCurve.Projective.dblU_eq {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} (P : Fin 3F) :
                              W.dblU P = (W.a₁ * P 1 * P 2 - (3 * P 0 ^ 2 + 2 * W.a₂ * P 0 * P 2 + W.a₄ * P 2 ^ 2)) ^ 3 / P 2 ^ 2
                              theorem WeierstrassCurve.Projective.dblU_smul {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hPz : P 2 0) {u : F} (hu : u 0) :
                              W.dblU (u P) = u ^ 4 * W.dblU P
                              theorem WeierstrassCurve.Projective.dblU_of_Z_eq_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hPz : P 2 = 0) :
                              W.dblU P = 0
                              theorem WeierstrassCurve.Projective.dblU_ne_zero_of_Y_eq {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Nonsingular P) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 = Q 1 * P 2) (hy' : P 1 * Q 2 = W.negY Q * P 2) :
                              W.dblU P 0
                              theorem WeierstrassCurve.Projective.isUnit_dblU_of_Y_eq {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Nonsingular P) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 = Q 1 * P 2) (hy' : P 1 * Q 2 = W.negY Q * P 2) :
                              IsUnit (W.dblU P)

                              The $Z$-coordinate of a representative of 2 • P for a point P.

                              Equations
                              • W'.dblZ P = P 2 * (P 1 - W'.negY P) ^ 3
                              Instances For
                                theorem WeierstrassCurve.Projective.dblZ_smul {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) (u : R) :
                                W'.dblZ (u P) = u ^ 4 * W'.dblZ P
                                theorem WeierstrassCurve.Projective.dblZ_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3R} (hPz : P 2 = 0) :
                                W'.dblZ P = 0
                                theorem WeierstrassCurve.Projective.dblZ_of_Y_eq {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 = Q 1 * P 2) (hy' : P 1 * Q 2 = W'.negY Q * P 2) :
                                W'.dblZ P = 0
                                theorem WeierstrassCurve.Projective.dblZ_ne_zero_of_Y_ne {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 Q 1 * P 2) :
                                W'.dblZ P 0
                                theorem WeierstrassCurve.Projective.isUnit_dblZ_of_Y_ne {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 Q 1 * P 2) :
                                IsUnit (W.dblZ P)
                                theorem WeierstrassCurve.Projective.dblZ_ne_zero_of_Y_ne' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 W'.negY Q * P 2) :
                                W'.dblZ P 0
                                theorem WeierstrassCurve.Projective.isUnit_dblZ_of_Y_ne' {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 W.negY Q * P 2) :
                                IsUnit (W.dblZ P)
                                noncomputable def WeierstrassCurve.Projective.dblX {R : Type u} (W' : WeierstrassCurve.Projective R) [CommRing R] (P : Fin 3R) :
                                R

                                The $X$-coordinate of a representative of 2 • P for a point P.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  theorem WeierstrassCurve.Projective.dblX_eq' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3R} (hP : W'.Equation P) :
                                  W'.dblX P * P 2 = ((MvPolynomial.eval P) W'.polynomialX ^ 2 - W'.a₁ * (MvPolynomial.eval P) W'.polynomialX * P 2 * (P 1 - W'.negY P) - W'.a₂ * P 2 ^ 2 * (P 1 - W'.negY P) ^ 2 - 2 * P 0 * P 2 * (P 1 - W'.negY P) ^ 2) * (P 1 - W'.negY P)
                                  theorem WeierstrassCurve.Projective.dblX_eq {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hP : W.Equation P) (hPz : P 2 0) :
                                  W.dblX P = ((MvPolynomial.eval P) W.polynomialX ^ 2 - W.a₁ * (MvPolynomial.eval P) W.polynomialX * P 2 * (P 1 - W.negY P) - W.a₂ * P 2 ^ 2 * (P 1 - W.negY P) ^ 2 - 2 * P 0 * P 2 * (P 1 - W.negY P) ^ 2) * (P 1 - W.negY P) / P 2
                                  theorem WeierstrassCurve.Projective.dblX_smul {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) (u : R) :
                                  W'.dblX (u P) = u ^ 4 * W'.dblX P
                                  theorem WeierstrassCurve.Projective.dblX_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} (hP : W'.Equation P) (hPz : P 2 = 0) :
                                  W'.dblX P = 0
                                  theorem WeierstrassCurve.Projective.dblX_of_Y_eq {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 = Q 1 * P 2) (hy' : P 1 * Q 2 = W'.negY Q * P 2) :
                                  W'.dblX P = 0
                                  theorem WeierstrassCurve.Projective.dblX_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 W.negY Q * P 2) :
                                  W.dblX P / W.dblZ P = W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))
                                  noncomputable def WeierstrassCurve.Projective.negDblY {R : Type u} (W' : WeierstrassCurve.Projective R) [CommRing R] (P : Fin 3R) :
                                  R

                                  The $Y$-coordinate of a representative of -(2 • P) for a point P.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    theorem WeierstrassCurve.Projective.negDblY_eq' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3R} (hP : W'.Equation P) :
                                    W'.negDblY P * P 2 ^ 2 = -(MvPolynomial.eval P) W'.polynomialX * ((MvPolynomial.eval P) W'.polynomialX ^ 2 - W'.a₁ * (MvPolynomial.eval P) W'.polynomialX * P 2 * (P 1 - W'.negY P) - W'.a₂ * P 2 ^ 2 * (P 1 - W'.negY P) ^ 2 - 2 * P 0 * P 2 * (P 1 - W'.negY P) ^ 2 - P 0 * P 2 * (P 1 - W'.negY P) ^ 2) + P 1 * P 2 ^ 2 * (P 1 - W'.negY P) ^ 3
                                    theorem WeierstrassCurve.Projective.negDblY_eq {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hP : W.Equation P) (hPz : P 2 0) :
                                    W.negDblY P = (-(MvPolynomial.eval P) W.polynomialX * ((MvPolynomial.eval P) W.polynomialX ^ 2 - W.a₁ * (MvPolynomial.eval P) W.polynomialX * P 2 * (P 1 - W.negY P) - W.a₂ * P 2 ^ 2 * (P 1 - W.negY P) ^ 2 - 2 * P 0 * P 2 * (P 1 - W.negY P) ^ 2 - P 0 * P 2 * (P 1 - W.negY P) ^ 2) + P 1 * P 2 ^ 2 * (P 1 - W.negY P) ^ 3) / P 2 ^ 2
                                    theorem WeierstrassCurve.Projective.negDblY_smul {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) (u : R) :
                                    W'.negDblY (u P) = u ^ 4 * W'.negDblY P
                                    theorem WeierstrassCurve.Projective.negDblY_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} (hP : W'.Equation P) (hPz : P 2 = 0) :
                                    W'.negDblY P = -P 1 ^ 4
                                    theorem WeierstrassCurve.Projective.negDblY_of_Y_eq' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 = Q 1 * P 2) (hy' : P 1 * Q 2 = W'.negY Q * P 2) :
                                    W'.negDblY P * P 2 ^ 2 = -(MvPolynomial.eval P) W'.polynomialX ^ 3
                                    theorem WeierstrassCurve.Projective.negDblY_of_Y_eq {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Equation P) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 = Q 1 * P 2) (hy' : P 1 * Q 2 = W.negY Q * P 2) :
                                    W.negDblY P = -W.dblU P
                                    theorem WeierstrassCurve.Projective.negDblY_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 W.negY Q * P 2) :
                                    W.negDblY P / W.dblZ P = W.toAffine.negAddY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))
                                    noncomputable def WeierstrassCurve.Projective.dblY {R : Type u} (W' : WeierstrassCurve.Projective R) [CommRing R] (P : Fin 3R) :
                                    R

                                    The $Y$-coordinate of a representative of 2 • P for a point P.

                                    Equations
                                    • W'.dblY P = W'.negY ![W'.dblX P, W'.negDblY P, W'.dblZ P]
                                    Instances For
                                      theorem WeierstrassCurve.Projective.dblY_smul {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) (u : R) :
                                      W'.dblY (u P) = u ^ 4 * W'.dblY P
                                      theorem WeierstrassCurve.Projective.dblY_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} (hP : W'.Equation P) (hPz : P 2 = 0) :
                                      W'.dblY P = P 1 ^ 4
                                      theorem WeierstrassCurve.Projective.dblY_of_Y_eq' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 = Q 1 * P 2) (hy' : P 1 * Q 2 = W'.negY Q * P 2) :
                                      W'.dblY P * P 2 ^ 2 = (MvPolynomial.eval P) W'.polynomialX ^ 3
                                      theorem WeierstrassCurve.Projective.dblY_of_Y_eq {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Equation P) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 = Q 1 * P 2) (hy' : P 1 * Q 2 = W.negY Q * P 2) :
                                      W.dblY P = W.dblU P
                                      theorem WeierstrassCurve.Projective.dblY_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 W.negY Q * P 2) :
                                      W.dblY P / W.dblZ P = W.toAffine.addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))
                                      noncomputable def WeierstrassCurve.Projective.dblXYZ {R : Type u} (W' : WeierstrassCurve.Projective R) [CommRing R] (P : Fin 3R) :
                                      Fin 3R

                                      The coordinates of a representative of 2 • P for a point P.

                                      Equations
                                      • W'.dblXYZ P = ![W'.dblX P, W'.dblY P, W'.dblZ P]
                                      Instances For
                                        theorem WeierstrassCurve.Projective.dblXYZ_X {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                                        W'.dblXYZ P 0 = W'.dblX P
                                        theorem WeierstrassCurve.Projective.dblXYZ_Y {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                                        W'.dblXYZ P 1 = W'.dblY P
                                        theorem WeierstrassCurve.Projective.dblXYZ_Z {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                                        W'.dblXYZ P 2 = W'.dblZ P
                                        theorem WeierstrassCurve.Projective.dblXYZ_smul {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) (u : R) :
                                        W'.dblXYZ (u P) = u ^ 4 W'.dblXYZ P
                                        theorem WeierstrassCurve.Projective.dblXYZ_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} (hP : W'.Equation P) (hPz : P 2 = 0) :
                                        W'.dblXYZ P = P 1 ^ 4 ![0, 1, 0]
                                        theorem WeierstrassCurve.Projective.dblXYZ_of_Y_eq {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Equation P) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 = Q 1 * P 2) (hy' : P 1 * Q 2 = W.negY Q * P 2) :
                                        W.dblXYZ P = W.dblU P ![0, 1, 0]
                                        theorem WeierstrassCurve.Projective.dblXYZ_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 W.negY Q * P 2) :
                                        W.dblXYZ P = W.dblZ P ![W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)), W.toAffine.addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)), 1]

                                        Addition formulae #

                                        def WeierstrassCurve.Projective.addU {F : Type v} [Field F] (P : Fin 3F) (Q : Fin 3F) :
                                        F

                                        The unit associated to the addition of a non-2-torsion point P with its negation. More specifically, the unit u such that W.add P Q = u • ![0, 1, 0] where P x / P z = Q x / Q z but P ≠ W.neg P.

                                        Equations
                                        Instances For
                                          theorem WeierstrassCurve.Projective.addU_smul {F : Type v} [Field F] {P : Fin 3F} {Q : Fin 3F} (hPz : P 2 0) (hQz : Q 2 0) {u : F} {v : F} (hu : u 0) (hv : v 0) :
                                          theorem WeierstrassCurve.Projective.addU_of_Z_eq_zero_left {F : Type v} [Field F] {P : Fin 3F} {Q : Fin 3F} (hPz : P 2 = 0) :
                                          theorem WeierstrassCurve.Projective.addU_of_Z_eq_zero_right {F : Type v} [Field F] {P : Fin 3F} {Q : Fin 3F} (hQz : Q 2 = 0) :
                                          theorem WeierstrassCurve.Projective.addU_ne_zero_of_Y_ne {F : Type v} [Field F] {P : Fin 3F} {Q : Fin 3F} (hPz : P 2 0) (hQz : Q 2 0) (hy : P 1 * Q 2 Q 1 * P 2) :
                                          theorem WeierstrassCurve.Projective.isUnit_addU_of_Y_ne {F : Type v} [Field F] {P : Fin 3F} {Q : Fin 3F} (hPz : P 2 0) (hQz : Q 2 0) (hy : P 1 * Q 2 Q 1 * P 2) :
                                          def WeierstrassCurve.Projective.addZ {R : Type u} (W' : WeierstrassCurve.Projective R) [CommRing R] (P : Fin 3R) (Q : Fin 3R) :
                                          R

                                          The $Z$-coordinate of a representative of P + Q for two distinct points P and Q. Note that this returns the value 0 if the representatives of P and Q are equal.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            theorem WeierstrassCurve.Projective.addZ_eq' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hQ : W'.Equation Q) :
                                            W'.addZ P Q * (P 2 * Q 2) = (P 0 * Q 2 - Q 0 * P 2) ^ 3
                                            theorem WeierstrassCurve.Projective.addZ_eq {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) :
                                            W.addZ P Q = (P 0 * Q 2 - Q 0 * P 2) ^ 3 / (P 2 * Q 2)
                                            theorem WeierstrassCurve.Projective.addZ_smul {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) (Q : Fin 3R) (u : R) (v : R) :
                                            W'.addZ (u P) (v Q) = (u * v) ^ 2 * W'.addZ P Q
                                            theorem WeierstrassCurve.Projective.addZ_self {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                                            W'.addZ P P = 0
                                            theorem WeierstrassCurve.Projective.addZ_of_Z_eq_zero_left {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hPz : P 2 = 0) :
                                            W'.addZ P Q = P 1 ^ 2 * Q 2 * Q 2
                                            theorem WeierstrassCurve.Projective.addZ_of_Z_eq_zero_right {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hQ : W'.Equation Q) (hQz : Q 2 = 0) :
                                            W'.addZ P Q = -(Q 1 ^ 2 * P 2) * P 2
                                            theorem WeierstrassCurve.Projective.addZ_of_X_eq {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) :
                                            W'.addZ P Q = 0
                                            theorem WeierstrassCurve.Projective.addZ_ne_zero_of_X_ne {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hx : P 0 * Q 2 Q 0 * P 2) :
                                            W'.addZ P Q 0
                                            theorem WeierstrassCurve.Projective.isUnit_addZ_of_X_ne {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Equation P) (hQ : W.Equation Q) (hx : P 0 * Q 2 Q 0 * P 2) :
                                            IsUnit (W.addZ P Q)
                                            def WeierstrassCurve.Projective.addX {R : Type u} (W' : WeierstrassCurve.Projective R) [CommRing R] (P : Fin 3R) (Q : Fin 3R) :
                                            R

                                            The $X$-coordinate of a representative of P + Q for two distinct points P and Q. Note that this returns the value 0 if the representatives of P and Q are equal.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              theorem WeierstrassCurve.Projective.addX_eq' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hQ : W'.Equation Q) :
                                              W'.addX P Q * (P 2 * Q 2) ^ 2 = ((P 1 * Q 2 - Q 1 * P 2) ^ 2 * P 2 * Q 2 + W'.a₁ * (P 1 * Q 2 - Q 1 * P 2) * P 2 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) - W'.a₂ * P 2 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 - P 0 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 - Q 0 * P 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2) * (P 0 * Q 2 - Q 0 * P 2)
                                              theorem WeierstrassCurve.Projective.addX_eq {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) :
                                              W.addX P Q = ((P 1 * Q 2 - Q 1 * P 2) ^ 2 * P 2 * Q 2 + W.a₁ * (P 1 * Q 2 - Q 1 * P 2) * P 2 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) - W.a₂ * P 2 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 - P 0 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 - Q 0 * P 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2) * (P 0 * Q 2 - Q 0 * P 2) / (P 2 * Q 2) ^ 2
                                              theorem WeierstrassCurve.Projective.addX_smul {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) (Q : Fin 3R) (u : R) (v : R) :
                                              W'.addX (u P) (v Q) = (u * v) ^ 2 * W'.addX P Q
                                              theorem WeierstrassCurve.Projective.addX_self {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                                              W'.addX P P = 0
                                              theorem WeierstrassCurve.Projective.addX_of_Z_eq_zero_left {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hPz : P 2 = 0) :
                                              W'.addX P Q = P 1 ^ 2 * Q 2 * Q 0
                                              theorem WeierstrassCurve.Projective.addX_of_Z_eq_zero_right {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hQ : W'.Equation Q) (hQz : Q 2 = 0) :
                                              W'.addX P Q = -(Q 1 ^ 2 * P 2) * P 0
                                              theorem WeierstrassCurve.Projective.addX_of_X_eq {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) :
                                              W'.addX P Q = 0
                                              theorem WeierstrassCurve.Projective.addX_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 Q 0 * P 2) :
                                              W.addX P Q / W.addZ P Q = W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))
                                              def WeierstrassCurve.Projective.negAddY {R : Type u} (W' : WeierstrassCurve.Projective R) [CommRing R] (P : Fin 3R) (Q : Fin 3R) :
                                              R

                                              The $Y$-coordinate of a representative of -(P + Q) for two distinct points P and Q. Note that this returns the value 0 if the representatives of P and Q are equal.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                theorem WeierstrassCurve.Projective.negAddY_eq' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hQ : W'.Equation Q) :
                                                W'.negAddY P Q * (P 2 * Q 2) ^ 2 = (P 1 * Q 2 - Q 1 * P 2) * ((P 1 * Q 2 - Q 1 * P 2) ^ 2 * P 2 * Q 2 + W'.a₁ * (P 1 * Q 2 - Q 1 * P 2) * P 2 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) - W'.a₂ * P 2 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 - P 0 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 - Q 0 * P 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 - P 0 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2) + P 1 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 3
                                                theorem WeierstrassCurve.Projective.negAddY_eq {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) :
                                                W.negAddY P Q = ((P 1 * Q 2 - Q 1 * P 2) * ((P 1 * Q 2 - Q 1 * P 2) ^ 2 * P 2 * Q 2 + W.a₁ * (P 1 * Q 2 - Q 1 * P 2) * P 2 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) - W.a₂ * P 2 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 - P 0 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 - Q 0 * P 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2 - P 0 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 2) + P 1 * Q 2 * (P 0 * Q 2 - Q 0 * P 2) ^ 3) / (P 2 * Q 2) ^ 2
                                                theorem WeierstrassCurve.Projective.negAddY_smul {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) (Q : Fin 3R) (u : R) (v : R) :
                                                W'.negAddY (u P) (v Q) = (u * v) ^ 2 * W'.negAddY P Q
                                                theorem WeierstrassCurve.Projective.negAddY_self {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                                                W'.negAddY P P = 0
                                                theorem WeierstrassCurve.Projective.negAddY_of_Z_eq_zero_left {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hPz : P 2 = 0) :
                                                W'.negAddY P Q = P 1 ^ 2 * Q 2 * W'.negY Q
                                                theorem WeierstrassCurve.Projective.negAddY_of_Z_eq_zero_right {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hQ : W'.Equation Q) (hQz : Q 2 = 0) :
                                                W'.negAddY P Q = -(Q 1 ^ 2 * P 2) * W'.negY P
                                                theorem WeierstrassCurve.Projective.negAddY_of_X_eq' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hx : P 0 * Q 2 = Q 0 * P 2) :
                                                W'.negAddY P Q * (P 2 * Q 2) ^ 2 = (P 1 * Q 2 - Q 1 * P 2) ^ 3 * (P 2 * Q 2)
                                                theorem WeierstrassCurve.Projective.negAddY_of_X_eq {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) :
                                                theorem WeierstrassCurve.Projective.negAddY_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 Q 0 * P 2) :
                                                W.negAddY P Q / W.addZ P Q = W.toAffine.negAddY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))
                                                def WeierstrassCurve.Projective.addY {R : Type u} (W' : WeierstrassCurve.Projective R) [CommRing R] (P : Fin 3R) (Q : Fin 3R) :
                                                R

                                                The $Y$-coordinate of a representative of P + Q for two distinct points P and Q. Note that this returns the value 0 if the representatives of P and Q are equal.

                                                Equations
                                                • W'.addY P Q = W'.negY ![W'.addX P Q, W'.negAddY P Q, W'.addZ P Q]
                                                Instances For
                                                  theorem WeierstrassCurve.Projective.addY_smul {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) (Q : Fin 3R) (u : R) (v : R) :
                                                  W'.addY (u P) (v Q) = (u * v) ^ 2 * W'.addY P Q
                                                  theorem WeierstrassCurve.Projective.addY_self {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                                                  W'.addY P P = 0
                                                  theorem WeierstrassCurve.Projective.addY_of_Z_eq_zero_left {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hPz : P 2 = 0) :
                                                  W'.addY P Q = P 1 ^ 2 * Q 2 * Q 1
                                                  theorem WeierstrassCurve.Projective.addY_of_Z_eq_zero_right {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hQ : W'.Equation Q) (hQz : Q 2 = 0) :
                                                  W'.addY P Q = -(Q 1 ^ 2 * P 2) * P 1
                                                  theorem WeierstrassCurve.Projective.addY_of_X_eq' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hQ : W'.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) :
                                                  W'.addY P Q * (P 2 * Q 2) ^ 3 = -(P 1 * Q 2 - Q 1 * P 2) ^ 3 * (P 2 * Q 2) ^ 2
                                                  theorem WeierstrassCurve.Projective.addY_of_X_eq {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) :
                                                  theorem WeierstrassCurve.Projective.addY_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 Q 0 * P 2) :
                                                  W.addY P Q / W.addZ P Q = W.toAffine.addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2))
                                                  noncomputable def WeierstrassCurve.Projective.addXYZ {R : Type u} (W' : WeierstrassCurve.Projective R) [CommRing R] (P : Fin 3R) (Q : Fin 3R) :
                                                  Fin 3R

                                                  The coordinates of a representative of P + Q for two distinct points P and Q. Note that this returns the value ![0, 0, 0] if the representatives of P and Q are equal.

                                                  Equations
                                                  • W'.addXYZ P Q = ![W'.addX P Q, W'.addY P Q, W'.addZ P Q]
                                                  Instances For
                                                    theorem WeierstrassCurve.Projective.addXYZ_X {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) (Q : Fin 3R) :
                                                    W'.addXYZ P Q 0 = W'.addX P Q
                                                    theorem WeierstrassCurve.Projective.addXYZ_Y {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) (Q : Fin 3R) :
                                                    W'.addXYZ P Q 1 = W'.addY P Q
                                                    theorem WeierstrassCurve.Projective.addXYZ_Z {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) (Q : Fin 3R) :
                                                    W'.addXYZ P Q 2 = W'.addZ P Q
                                                    theorem WeierstrassCurve.Projective.addXYZ_smul {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) (Q : Fin 3R) (u : R) (v : R) :
                                                    W'.addXYZ (u P) (v Q) = (u * v) ^ 2 W'.addXYZ P Q
                                                    theorem WeierstrassCurve.Projective.addXYZ_self {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                                                    W'.addXYZ P P = ![0, 0, 0]
                                                    theorem WeierstrassCurve.Projective.addXYZ_of_Z_eq_zero_left {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hP : W'.Equation P) (hPz : P 2 = 0) :
                                                    W'.addXYZ P Q = (P 1 ^ 2 * Q 2) Q
                                                    theorem WeierstrassCurve.Projective.addXYZ_of_Z_eq_zero_right {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3R} {Q : Fin 3R} (hQ : W'.Equation Q) (hQz : Q 2 = 0) :
                                                    W'.addXYZ P Q = -(Q 1 ^ 2 * P 2) P
                                                    theorem WeierstrassCurve.Projective.addXYZ_of_X_eq {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 = Q 0 * P 2) :
                                                    W.addXYZ P Q = WeierstrassCurve.Projective.addU P Q ![0, 1, 0]
                                                    theorem WeierstrassCurve.Projective.addXYZ_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hx : P 0 * Q 2 Q 0 * P 2) :
                                                    W.addXYZ P Q = W.addZ P Q ![W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)), W.toAffine.addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)), 1]