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. This file also defines the negation and addition operations of the group law for this type, and proves that they respect the Weierstrass equation and the nonsingular condition. The fact that they form an abelian group is proven in Mathlib.AlgebraicGeometry.EllipticCurve.Group.

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. Note that most computational proofs follow from their analogous proofs for affine coordinates.

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 Y 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 Y 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
          theorem WeierstrassCurve.Projective.smul_equiv_smul {R : Type u} [CommRing R] (P Q : Fin 3R) {u v : R} (hu : IsUnit u) (hv : IsUnit v) :
          u P v Q P Q
          @[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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 Y 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 Q : Fin 3F} (hPz : P 2 0) (hQz : Q 2 0) {u v : F} (hu : u 0) (hv : v 0) :
                                          theorem WeierstrassCurve.Projective.addU_ne_zero_of_Y_ne {F : Type v} [Field F] {P 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 Q : Fin 3F} (hPz : P 2 0) (hQz : Q 2 0) (hy : P 1 * Q 2 Q 1 * P 2) :

                                          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 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 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 Q : Fin 3R) (u 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 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 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 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 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 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)

                                            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 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 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 Q : Fin 3R) (u 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 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 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 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 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))

                                              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 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 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 Q : Fin 3R) (u 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 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 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 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 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 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))

                                                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 Q : Fin 3R) (u 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 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 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 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 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 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 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 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 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 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 Q : Fin 3R) (u 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 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 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 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 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]

                                                    Negation on point representatives #

                                                    def WeierstrassCurve.Projective.neg {R : Type u} (W' : WeierstrassCurve.Projective R) [CommRing R] (P : Fin 3R) :
                                                    Fin 3R

                                                    The negation of a point representative.

                                                    Equations
                                                    • W'.neg P = ![P 0, W'.negY P, P 2]
                                                    Instances For
                                                      theorem WeierstrassCurve.Projective.neg_X {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                                                      W'.neg P 0 = P 0
                                                      theorem WeierstrassCurve.Projective.neg_Y {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                                                      W'.neg P 1 = W'.negY P
                                                      theorem WeierstrassCurve.Projective.neg_Z {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                                                      W'.neg P 2 = P 2
                                                      theorem WeierstrassCurve.Projective.neg_smul {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) (u : R) :
                                                      W'.neg (u P) = u W'.neg P
                                                      theorem WeierstrassCurve.Projective.neg_smul_equiv {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) {u : R} (hu : IsUnit u) :
                                                      W'.neg (u P) W'.neg P
                                                      theorem WeierstrassCurve.Projective.neg_equiv {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P Q : Fin 3R} (h : P Q) :
                                                      W'.neg P W'.neg Q
                                                      theorem WeierstrassCurve.Projective.neg_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'.neg P = -P 1 ![0, 1, 0]
                                                      theorem WeierstrassCurve.Projective.neg_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hPz : P 2 0) :
                                                      W.neg P = P 2 ![P 0 / P 2, W.toAffine.negY (P 0 / P 2) (P 1 / P 2), 1]
                                                      theorem WeierstrassCurve.Projective.nonsingular_neg {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hP : W.Nonsingular P) :
                                                      W.Nonsingular (W.neg P)
                                                      theorem WeierstrassCurve.Projective.addZ_neg {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                                                      W'.addZ P (W'.neg P) = 0
                                                      theorem WeierstrassCurve.Projective.addX_neg {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                                                      W'.addX P (W'.neg P) = 0
                                                      theorem WeierstrassCurve.Projective.negAddY_neg {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3R} (hP : W'.Equation P) :
                                                      W'.negAddY P (W'.neg P) = W'.dblZ P
                                                      theorem WeierstrassCurve.Projective.addY_neg {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3R} (hP : W'.Equation P) :
                                                      W'.addY P (W'.neg P) = -W'.dblZ P
                                                      theorem WeierstrassCurve.Projective.addXYZ_neg {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3R} (hP : W'.Equation P) :
                                                      W'.addXYZ P (W'.neg P) = -W'.dblZ P ![0, 1, 0]

                                                      The negation of a point class. If P is a point representative, then W'.negMap ⟦P⟧ is definitionally equivalent to W'.neg P.

                                                      Equations
                                                      Instances For
                                                        theorem WeierstrassCurve.Projective.negMap_eq {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                                                        W'.negMap P = W'.neg P
                                                        theorem WeierstrassCurve.Projective.negMap_of_Z_eq_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hP : W.Nonsingular P) (hPz : P 2 = 0) :
                                                        W.negMap P = ![0, 1, 0]
                                                        theorem WeierstrassCurve.Projective.negMap_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hPz : P 2 0) :
                                                        W.negMap P = ![P 0 / P 2, W.toAffine.negY (P 0 / P 2) (P 1 / P 2), 1]
                                                        theorem WeierstrassCurve.Projective.nonsingularLift_negMap {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : WeierstrassCurve.Projective.PointClass F} (hP : W.NonsingularLift P) :
                                                        W.NonsingularLift (W.negMap P)

                                                        Addition on point representatives #

                                                        noncomputable def WeierstrassCurve.Projective.add {R : Type u} (W' : WeierstrassCurve.Projective R) [CommRing R] (P Q : Fin 3R) :
                                                        Fin 3R

                                                        The addition of two point representatives.

                                                        Equations
                                                        • W'.add P Q = if P Q then W'.dblXYZ P else W'.addXYZ P Q
                                                        Instances For
                                                          theorem WeierstrassCurve.Projective.add_of_equiv {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P Q : Fin 3R} (h : P Q) :
                                                          W'.add P Q = W'.dblXYZ P
                                                          theorem WeierstrassCurve.Projective.add_smul_of_equiv {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P Q : Fin 3R} (h : P Q) {u v : R} (hu : IsUnit u) (hv : IsUnit v) :
                                                          W'.add (u P) (v Q) = u ^ 4 W'.add P Q
                                                          theorem WeierstrassCurve.Projective.add_self {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3R) :
                                                          W'.add P P = W'.dblXYZ P
                                                          theorem WeierstrassCurve.Projective.add_of_eq {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P Q : Fin 3R} (h : P = Q) :
                                                          W'.add P Q = W'.dblXYZ P
                                                          theorem WeierstrassCurve.Projective.add_of_not_equiv {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P Q : Fin 3R} (h : ¬P Q) :
                                                          W'.add P Q = W'.addXYZ P Q
                                                          theorem WeierstrassCurve.Projective.add_smul_of_not_equiv {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P Q : Fin 3R} (h : ¬P Q) {u v : R} (hu : IsUnit u) (hv : IsUnit v) :
                                                          W'.add (u P) (v Q) = (u * v) ^ 2 W'.add P Q
                                                          theorem WeierstrassCurve.Projective.add_smul_equiv {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P Q : Fin 3R) {u v : R} (hu : IsUnit u) (hv : IsUnit v) :
                                                          W'.add (u P) (v Q) W'.add P Q
                                                          theorem WeierstrassCurve.Projective.add_equiv {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P P' Q Q' : Fin 3R} (hP : P P') (hQ : Q Q') :
                                                          W'.add P Q W'.add P' Q'
                                                          theorem WeierstrassCurve.Projective.add_of_Z_eq_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) (hPz : P 2 = 0) (hQz : Q 2 = 0) :
                                                          W.add P Q = P 1 ^ 4 ![0, 1, 0]
                                                          theorem WeierstrassCurve.Projective.add_of_Z_eq_zero_left {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P Q : Fin 3R} (hP : W'.Equation P) (hPz : P 2 = 0) (hQz : Q 2 0) :
                                                          W'.add P Q = (P 1 ^ 2 * Q 2) Q
                                                          theorem WeierstrassCurve.Projective.add_of_Z_eq_zero_right {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P Q : Fin 3R} (hQ : W'.Equation Q) (hPz : P 2 0) (hQz : Q 2 = 0) :
                                                          W'.add P Q = -(Q 1 ^ 2 * P 2) P
                                                          theorem WeierstrassCurve.Projective.add_of_Y_eq {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P 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.add P Q = W.dblU P ![0, 1, 0]
                                                          theorem WeierstrassCurve.Projective.add_of_Y_ne {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P 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) :
                                                          W.add P Q = WeierstrassCurve.Projective.addU P Q ![0, 1, 0]
                                                          theorem WeierstrassCurve.Projective.add_of_Y_ne' {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P 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.add P Q = 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]
                                                          theorem WeierstrassCurve.Projective.add_of_X_ne {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P 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.add 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]
                                                          theorem WeierstrassCurve.Projective.nonsingular_add {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) :
                                                          W.Nonsingular (W.add P Q)

                                                          The addition of two point classes. If P is a point representative, then W.addMap ⟦P⟧ ⟦Q⟧ is definitionally equivalent to W.add P Q.

                                                          Equations
                                                          Instances For
                                                            theorem WeierstrassCurve.Projective.addMap_eq {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P Q : Fin 3R) :
                                                            W'.addMap P Q = W'.add P Q
                                                            theorem WeierstrassCurve.Projective.addMap_of_Z_eq_zero_left {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : WeierstrassCurve.Projective.PointClass F} (hP : W.Nonsingular P) (hQ : W.NonsingularLift Q) (hPz : P 2 = 0) :
                                                            W.addMap P Q = Q
                                                            theorem WeierstrassCurve.Projective.addMap_of_Z_eq_zero_right {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : WeierstrassCurve.Projective.PointClass F} {Q : Fin 3F} (hP : W.NonsingularLift P) (hQ : W.Nonsingular Q) (hQz : Q 2 = 0) :
                                                            W.addMap P Q = P
                                                            theorem WeierstrassCurve.Projective.addMap_of_Y_eq {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3F} (hP : W.Nonsingular 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.addMap P Q = ![0, 1, 0]
                                                            theorem WeierstrassCurve.Projective.addMap_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P 2 0) (hQz : Q 2 0) (hxy : P 0 * Q 2 = Q 0 * P 2P 1 * Q 2 W.negY Q * P 2) :
                                                            W.addMap 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]
                                                            theorem WeierstrassCurve.Projective.nonsingularLift_addMap {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P Q : WeierstrassCurve.Projective.PointClass F} (hP : W.NonsingularLift P) (hQ : W.NonsingularLift Q) :
                                                            W.NonsingularLift (W.addMap P Q)

                                                            Nonsingular rational points #

                                                            A nonsingular rational point on W'.

                                                            • The point class underlying a nonsingular rational point on W'.

                                                            • nonsingular : W'.NonsingularLift self.point

                                                              The nonsingular condition underlying a nonsingular rational point on W'.

                                                            Instances For
                                                              theorem WeierstrassCurve.Projective.Point.ext {R : Type u} {W' : WeierstrassCurve.Projective R} {inst✝ : CommRing R} {x y : W'.Point} (point : x.point = y.point) :
                                                              x = y
                                                              Equations
                                                              def WeierstrassCurve.Projective.Point.fromAffine {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [Nontrivial R] :
                                                              W'.toAffine.PointW'.Point

                                                              The map from a nonsingular rational point on a Weierstrass curve W' in affine coordinates to the corresponding nonsingular rational point on W' in projective coordinates.

                                                              Equations
                                                              Instances For
                                                                def WeierstrassCurve.Projective.Point.neg {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} (P : W.Point) :
                                                                W.Point

                                                                The negation of a nonsingular rational point on W. Given a nonsingular rational point P on W, use -P instead of neg P.

                                                                Equations
                                                                Instances For
                                                                  Equations
                                                                  • WeierstrassCurve.Projective.Point.instNegPoint = { neg := WeierstrassCurve.Projective.Point.neg }
                                                                  theorem WeierstrassCurve.Projective.Point.neg_point {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} (P : W.Point) :
                                                                  (-P).point = W.negMap P.point
                                                                  noncomputable def WeierstrassCurve.Projective.Point.add {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} (P Q : W.Point) :
                                                                  W.Point

                                                                  The addition of two nonsingular rational points on W. Given two nonsingular rational points P and Q on W, use P + Q instead of add P Q.

                                                                  Equations
                                                                  Instances For
                                                                    Equations
                                                                    • WeierstrassCurve.Projective.Point.instAddPoint = { add := WeierstrassCurve.Projective.Point.add }
                                                                    theorem WeierstrassCurve.Projective.Point.add_def {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} (P Q : W.Point) :
                                                                    P + Q = P.add Q
                                                                    theorem WeierstrassCurve.Projective.Point.add_point {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} (P Q : W.Point) :
                                                                    (P + Q).point = W.addMap P.point Q.point

                                                                    Equivalence with affine coordinates #

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

                                                                    The map from a point representative that is nonsingular on a Weierstrass curve W in projective coordinates to the corresponding nonsingular rational point on W in affine coordinates.

                                                                    Equations
                                                                    Instances For
                                                                      noncomputable def WeierstrassCurve.Projective.Point.toAffineLift {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} (P : W.Point) :
                                                                      W.toAffine.Point

                                                                      The map from a nonsingular rational point on a Weierstrass curve W in projective coordinates to the corresponding nonsingular rational point on W in affine coordinates.

                                                                      Equations
                                                                      Instances For
                                                                        theorem WeierstrassCurve.Projective.Point.toAffineLift_of_Z_eq_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hP : W.NonsingularLift P) (hPz : P 2 = 0) :
                                                                        theorem WeierstrassCurve.Projective.Point.toAffineLift_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {hP : W.NonsingularLift P} (hPz : P 2 0) :
                                                                        theorem WeierstrassCurve.Projective.Point.toAffineLift_neg {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} (P : W.Point) :
                                                                        (-P).toAffineLift = -P.toAffineLift
                                                                        theorem WeierstrassCurve.Projective.Point.toAffineLift_add {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} (P Q : W.Point) :
                                                                        (P + Q).toAffineLift = P.toAffineLift + Q.toAffineLift
                                                                        noncomputable def WeierstrassCurve.Projective.Point.toAffineAddEquiv {F : Type v} [Field F] (W : WeierstrassCurve.Projective F) :
                                                                        W.Point ≃+ W.toAffine.Point

                                                                        The equivalence between the nonsingular rational points on a Weierstrass curve W in Projective coordinates with the nonsingular rational points on W in affine coordinates.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          @[reducible, inline]

                                                                          An abbreviation for WeierstrassCurve.Projective.Point.fromAffine for dot notation.

                                                                          Equations
                                                                          Instances For