Documentation

Mathlib.AlgebraicGeometry.EllipticCurve.Affine

Affine coordinates for Weierstrass curves #

This file defines the type of points on a Weierstrass curve as an inductive, consisting of the point at infinity and affine points 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 rational point on W is simply a point $[X:Y:Z]$ defined over F in the projective plane satisfying the homogeneous cubic equation $Y^2Z + a_1XYZ + a_3YZ^2 = X^3 + a_2X^2Z + a_4XZ^2 + a_6Z^3$. Any such point either lies in the affine chart $Z \ne 0$ and satisfies the Weierstrass equation obtained by replacing $X/Z$ with $X$ and $Y/Z$ with $Y$, or is the unique point at infinity $0 := [0:1:0]$ when $Z = 0$. With this new description, a nonsingular rational point on W is either $0$ or an affine point $(x, y)$ where the partial derivatives $W_X(X, Y)$ and $W_Y(X, Y)$ do not vanish simultaneously. For a field extension K of F, a K-rational point is simply a rational point on W base changed to K.

The set of nonsingular rational points forms an abelian group under a secant-and-tangent process.

The group law on this set is then uniquely determined by these constructions.

Main definitions #

Main statements #

Notations #

References #

[J Silverman, The Arithmetic of Elliptic Curves][silverman2009]

Tags #

elliptic curve, rational point, affine coordinates

Weierstrass curves #

@[reducible, inline]

An abbreviation for a Weierstrass curve in affine coordinates.

Equations
Instances For
    @[reducible, inline]

    The coercion to a Weierstrass curve in affine coordinates.

    Equations
    • W.toAffine = W
    Instances For

      Weierstrass equations #

      The polynomial $W(X, Y) := Y^2 + a_1XY + a_3Y - (X^3 + a_2X^2 + a_4X + a_6)$ associated to a Weierstrass curve W over R. For ease of polynomial manipulation, this is represented as a term of type R[X][X], where the inner variable represents $X$ and the outer variable represents $Y$. For clarity, the alternative notations Y and R[X][Y] are provided in the Polynomial scope to represent the outer variable and the bivariate polynomial ring R[X][X] respectively.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem WeierstrassCurve.Affine.polynomial_eq {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) :
        W.polynomial = { a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly, d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly }.toPoly
        @[simp]
        theorem WeierstrassCurve.Affine.degree_polynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) [Nontrivial R] :
        W.polynomial.degree = 2
        @[simp]
        theorem WeierstrassCurve.Affine.natDegree_polynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) [Nontrivial R] :
        W.polynomial.natDegree = 2
        theorem WeierstrassCurve.Affine.evalEval_polynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) :
        Polynomial.evalEval x y W.polynomial = y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆)

        The proposition that an affine point $(x, y)$ lies in W. In other words, $W(x, y) = 0$.

        Equations
        Instances For
          theorem WeierstrassCurve.Affine.equation_iff' {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) :
          W.Equation x y y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = 0
          theorem WeierstrassCurve.Affine.equation_iff {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) :
          W.Equation x y y ^ 2 + W.a₁ * x * y + W.a₃ * y = x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆
          @[simp]
          theorem WeierstrassCurve.Affine.equation_zero {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) :
          W.Equation 0 0 W.a₆ = 0
          theorem WeierstrassCurve.Affine.equation_iff_variableChange {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) :
          W.Equation x y (WeierstrassCurve.variableChange W { u := 1, r := x, s := 0, t := y }).toAffine.Equation 0 0

          Nonsingular Weierstrass equations #

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

          TODO: define this in terms of Polynomial.derivative.

          Equations
          • W.polynomialX = Polynomial.C (Polynomial.C W.a₁) * Polynomial.X - Polynomial.C (Polynomial.C 3 * Polynomial.X ^ 2 + Polynomial.C (2 * W.a₂) * Polynomial.X + Polynomial.C W.a₄)
          Instances For
            theorem WeierstrassCurve.Affine.evalEval_polynomialX {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) :
            Polynomial.evalEval x y W.polynomialX = W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)

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

            TODO: define this in terms of Polynomial.derivative.

            Equations
            • W.polynomialY = Polynomial.C (Polynomial.C 2) * Polynomial.X + Polynomial.C (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃)
            Instances For
              theorem WeierstrassCurve.Affine.evalEval_polynomialY {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) :
              Polynomial.evalEval x y W.polynomialY = 2 * y + W.a₁ * x + W.a₃
              @[deprecated WeierstrassCurve.Affine.evalEval_polynomial]
              theorem WeierstrassCurve.Affine.eval_polynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) :
              Polynomial.evalEval x y W.polynomial = y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆)

              Alias of WeierstrassCurve.Affine.evalEval_polynomial.

              @[deprecated WeierstrassCurve.Affine.evalEval_polynomial_zero]

              Alias of WeierstrassCurve.Affine.evalEval_polynomial_zero.

              @[deprecated WeierstrassCurve.Affine.evalEval_polynomialX]
              theorem WeierstrassCurve.Affine.eval_polynomialX {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) :
              Polynomial.evalEval x y W.polynomialX = W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)

              Alias of WeierstrassCurve.Affine.evalEval_polynomialX.

              @[deprecated WeierstrassCurve.Affine.evalEval_polynomialX_zero]

              Alias of WeierstrassCurve.Affine.evalEval_polynomialX_zero.

              @[deprecated WeierstrassCurve.Affine.evalEval_polynomialY]
              theorem WeierstrassCurve.Affine.eval_polynomialY {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) :
              Polynomial.evalEval x y W.polynomialY = 2 * y + W.a₁ * x + W.a₃

              Alias of WeierstrassCurve.Affine.evalEval_polynomialY.

              @[deprecated WeierstrassCurve.Affine.evalEval_polynomialY_zero]

              Alias of WeierstrassCurve.Affine.evalEval_polynomialY_zero.

              The proposition that an affine point $(x, y)$ in W is nonsingular. In other words, either $W_X(x, y) \ne 0$ or $W_Y(x, y) \ne 0$.

              Note that this definition is only mathematically accurate for fields. TODO: generalise this definition to be mathematically accurate for a larger class of rings.

              Equations
              Instances For
                theorem WeierstrassCurve.Affine.nonsingular_iff' {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) :
                W.Nonsingular x y W.Equation x y (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) 0 2 * y + W.a₁ * x + W.a₃ 0)
                theorem WeierstrassCurve.Affine.nonsingular_iff {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) :
                W.Nonsingular x y W.Equation x y (W.a₁ * y 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ y -y - W.a₁ * x - W.a₃)
                @[simp]
                theorem WeierstrassCurve.Affine.nonsingular_zero {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) :
                W.Nonsingular 0 0 W.a₆ = 0 (W.a₃ 0 W.a₄ 0)
                theorem WeierstrassCurve.Affine.nonsingular_iff_variableChange {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) :
                W.Nonsingular x y (WeierstrassCurve.variableChange W { u := 1, r := x, s := 0, t := y }).toAffine.Nonsingular 0 0
                theorem WeierstrassCurve.Affine.nonsingular_zero_of_Δ_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (h : W.Equation 0 0) (hΔ : WeierstrassCurve.Δ W 0) :
                W.Nonsingular 0 0
                theorem WeierstrassCurve.Affine.nonsingular_of_Δ_ne_zero {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) {x : R} {y : R} (h : W.Equation x y) (hΔ : WeierstrassCurve.Δ W 0) :
                W.Nonsingular x y

                A Weierstrass curve is nonsingular at every point if its discriminant is non-zero.

                Group operation polynomials over a ring #

                The polynomial $-Y - a_1X - a_3$ associated to negation.

                Equations
                • W.negPolynomial = -Polynomial.X - Polynomial.C (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃)
                Instances For
                  theorem WeierstrassCurve.Affine.Y_sub_polynomialY {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) :
                  Polynomial.X - W.polynomialY = W.negPolynomial
                  theorem WeierstrassCurve.Affine.Y_sub_negPolynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) :
                  Polynomial.X - W.negPolynomial = W.polynomialY
                  def WeierstrassCurve.Affine.negY {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) :
                  R

                  The $Y$-coordinate of the negation of an affine point in W.

                  This depends on W, and has argument order: $x$, $y$.

                  Equations
                  • W.negY x y = -y - W.a₁ * x - W.a₃
                  Instances For
                    theorem WeierstrassCurve.Affine.negY_negY {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) :
                    W.negY x (W.negY x y) = y
                    theorem WeierstrassCurve.Affine.eval_negPolynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) :
                    Polynomial.evalEval x y W.negPolynomial = W.negY x y
                    noncomputable def WeierstrassCurve.Affine.linePolynomial {R : Type u} [CommRing R] (x : R) (y : R) (L : R) :

                    The polynomial $L(X - x) + y$ associated to the line $Y = L(X - x) + y$, with a slope of $L$ that passes through an affine point $(x, y)$.

                    This does not depend on W, and has argument order: $x$, $y$, $L$.

                    Equations
                    Instances For
                      noncomputable def WeierstrassCurve.Affine.addPolynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) (L : R) :

                      The polynomial obtained by substituting the line $Y = L*(X - x) + y$, with a slope of $L$ that passes through an affine point $(x, y)$, into the polynomial $W(X, Y)$ associated to W. If such a line intersects W at another point $(x', y')$, then the roots of this polynomial are precisely $x$, $x'$, and the $X$-coordinate of the addition of $(x, y)$ and $(x', y')$.

                      This depends on W, and has argument order: $x$, $y$, $L$.

                      Equations
                      Instances For
                        theorem WeierstrassCurve.Affine.C_addPolynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) (L : R) :
                        Polynomial.C (W.addPolynomial x y L) = (Polynomial.X - Polynomial.C (WeierstrassCurve.Affine.linePolynomial x y L)) * (W.negPolynomial - Polynomial.C (WeierstrassCurve.Affine.linePolynomial x y L)) + W.polynomial
                        theorem WeierstrassCurve.Affine.addPolynomial_eq {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) (L : R) :
                        W.addPolynomial x y L = -{ a := 1, b := -L ^ 2 - W.a₁ * L + W.a₂, c := 2 * x * L ^ 2 + (W.a₁ * x - 2 * y - W.a₃) * L + (-W.a₁ * y + W.a₄), d := -x ^ 2 * L ^ 2 + (2 * x * y + W.a₃ * x) * L - (y ^ 2 + W.a₃ * y - W.a₆) }.toPoly
                        def WeierstrassCurve.Affine.addX {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x₁ : R) (x₂ : R) (L : R) :
                        R

                        The $X$-coordinate of the addition of two affine points $(x_1, y_1)$ and $(x_2, y_2)$ in W, where the line through them is not vertical and has a slope of $L$.

                        This depends on W, and has argument order: $x_1$, $x_2$, $L$.

                        Equations
                        • W.addX x₁ x₂ L = L ^ 2 + W.a₁ * L - W.a₂ - x₁ - x₂
                        Instances For
                          def WeierstrassCurve.Affine.negAddY {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x₁ : R) (x₂ : R) (y₁ : R) (L : R) :
                          R

                          The $Y$-coordinate of the negated addition of two affine points $(x_1, y_1)$ and $(x_2, y_2)$, where the line through them is not vertical and has a slope of $L$.

                          This depends on W, and has argument order: $x_1$, $x_2$, $y_1$, $L$.

                          Equations
                          • W.negAddY x₁ x₂ y₁ L = L * (W.addX x₁ x₂ L - x₁) + y₁
                          Instances For
                            def WeierstrassCurve.Affine.addY {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x₁ : R) (x₂ : R) (y₁ : R) (L : R) :
                            R

                            The $Y$-coordinate of the addition of two affine points $(x_1, y_1)$ and $(x_2, y_2)$ in W, where the line through them is not vertical and has a slope of $L$.

                            This depends on W, and has argument order: $x_1$, $x_2$, $y_1$, $L$.

                            Equations
                            • W.addY x₁ x₂ y₁ L = W.negY (W.addX x₁ x₂ L) (W.negAddY x₁ x₂ y₁ L)
                            Instances For
                              theorem WeierstrassCurve.Affine.equation_neg_iff {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) :
                              W.Equation x (W.negY x y) W.Equation x y
                              theorem WeierstrassCurve.Affine.nonsingular_neg_iff {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) :
                              W.Nonsingular x (W.negY x y) W.Nonsingular x y
                              theorem WeierstrassCurve.Affine.equation_add_iff {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x₁ : R) (x₂ : R) (y₁ : R) (L : R) :
                              W.Equation (W.addX x₁ x₂ L) (W.negAddY x₁ x₂ y₁ L) Polynomial.eval (W.addX x₁ x₂ L) (W.addPolynomial x₁ y₁ L) = 0
                              theorem WeierstrassCurve.Affine.equation_neg_of {R : Type u} [CommRing R] {W : WeierstrassCurve.Affine R} {x : R} {y : R} (h : W.Equation x (W.negY x y)) :
                              W.Equation x y
                              theorem WeierstrassCurve.Affine.equation_neg {R : Type u} [CommRing R] {W : WeierstrassCurve.Affine R} {x : R} {y : R} (h : W.Equation x y) :
                              W.Equation x (W.negY x y)

                              The negation of an affine point in W lies in W.

                              theorem WeierstrassCurve.Affine.nonsingular_neg_of {R : Type u} [CommRing R] {W : WeierstrassCurve.Affine R} {x : R} {y : R} (h : W.Nonsingular x (W.negY x y)) :
                              W.Nonsingular x y
                              theorem WeierstrassCurve.Affine.nonsingular_neg {R : Type u} [CommRing R] {W : WeierstrassCurve.Affine R} {x : R} {y : R} (h : W.Nonsingular x y) :
                              W.Nonsingular x (W.negY x y)

                              The negation of a nonsingular affine point in W is nonsingular.

                              theorem WeierstrassCurve.Affine.nonsingular_negAdd_of_eval_derivative_ne_zero {R : Type u} [CommRing R] {W : WeierstrassCurve.Affine R} {x₁ : R} {x₂ : R} {y₁ : R} {L : R} (hx' : W.Equation (W.addX x₁ x₂ L) (W.negAddY x₁ x₂ y₁ L)) (hx : Polynomial.eval (W.addX x₁ x₂ L) (Polynomial.derivative (W.addPolynomial x₁ y₁ L)) 0) :
                              W.Nonsingular (W.addX x₁ x₂ L) (W.negAddY x₁ x₂ y₁ L)

                              Group operation polynomials over a field #

                              noncomputable def WeierstrassCurve.Affine.slope {F : Type u} [Field F] (W : WeierstrassCurve.Affine F) (x₁ : F) (x₂ : F) (y₁ : F) (y₂ : F) :
                              F

                              The slope of the line through two affine points $(x_1, y_1)$ and $(x_2, y_2)$ in W. If $x_1 \ne x_2$, then this line is the secant of W through $(x_1, y_1)$ and $(x_2, y_2)$, and has slope $(y_1 - y_2) / (x_1 - x_2)$. Otherwise, if $y_1 \ne -y_1 - a_1x_1 - a_3$, then this line is the tangent of W at $(x_1, y_1) = (x_2, y_2)$, and has slope $(3x_1^2 + 2a_2x_1 + a_4 - a_1y_1) / (2y_1 + a_1x_1 + a_3)$. Otherwise, this line is vertical, and has undefined slope, in which case this function returns the value 0.

                              This depends on W, and has argument order: $x_1$, $x_2$, $y_1$, $y_2$.

                              Equations
                              • W.slope x₁ x₂ y₁ y₂ = if x₁ = x₂ then if y₁ = W.negY x₂ y₂ then 0 else (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁) else (y₁ - y₂) / (x₁ - x₂)
                              Instances For
                                @[simp]
                                theorem WeierstrassCurve.Affine.slope_of_Y_eq {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (hx : x₁ = x₂) (hy : y₁ = W.negY x₂ y₂) :
                                W.slope x₁ x₂ y₁ y₂ = 0
                                @[simp]
                                theorem WeierstrassCurve.Affine.slope_of_Y_ne {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (hx : x₁ = x₂) (hy : y₁ W.negY x₂ y₂) :
                                W.slope x₁ x₂ y₁ y₂ = (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)
                                @[simp]
                                theorem WeierstrassCurve.Affine.slope_of_X_ne {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (hx : x₁ x₂) :
                                W.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂)
                                theorem WeierstrassCurve.Affine.slope_of_Y_ne_eq_eval {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (hx : x₁ = x₂) (hy : y₁ W.negY x₂ y₂) :
                                W.slope x₁ x₂ y₁ y₂ = -Polynomial.evalEval x₁ y₁ W.polynomialX / Polynomial.evalEval x₁ y₁ W.polynomialY
                                theorem WeierstrassCurve.Affine.Y_eq_of_X_eq {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hx : x₁ = x₂) :
                                y₁ = y₂ y₁ = W.negY x₂ y₂
                                theorem WeierstrassCurve.Affine.Y_eq_of_Y_ne {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hx : x₁ = x₂) (hy : y₁ W.negY x₂ y₂) :
                                y₁ = y₂
                                theorem WeierstrassCurve.Affine.addPolynomial_slope {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hxy : x₁ = x₂y₁ W.negY x₂ y₂) :
                                W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂) = -((Polynomial.X - Polynomial.C x₁) * (Polynomial.X - Polynomial.C x₂) * (Polynomial.X - Polynomial.C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))
                                theorem WeierstrassCurve.Affine.equation_negAdd {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hxy : x₁ = x₂y₁ W.negY x₂ y₂) :
                                W.Equation (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

                                The negated addition of two affine points in W on a sloped line lies in W.

                                theorem WeierstrassCurve.Affine.equation_add {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hxy : x₁ = x₂y₁ W.negY x₂ y₂) :
                                W.Equation (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

                                The addition of two affine points in W on a sloped line lies in W.

                                theorem WeierstrassCurve.Affine.derivative_addPolynomial_slope {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hxy : x₁ = x₂y₁ W.negY x₂ y₂) :
                                Polynomial.derivative (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) = -((Polynomial.X - Polynomial.C x₁) * (Polynomial.X - Polynomial.C x₂) + (Polynomial.X - Polynomial.C x₁) * (Polynomial.X - Polynomial.C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) + (Polynomial.X - Polynomial.C x₂) * (Polynomial.X - Polynomial.C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))
                                theorem WeierstrassCurve.Affine.nonsingular_negAdd {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : W.Nonsingular x₁ y₁) (h₂ : W.Nonsingular x₂ y₂) (hxy : x₁ = x₂y₁ W.negY x₂ y₂) :
                                W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

                                The negated addition of two nonsingular affine points in W on a sloped line is nonsingular.

                                theorem WeierstrassCurve.Affine.nonsingular_add {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : W.Nonsingular x₁ y₁) (h₂ : W.Nonsingular x₂ y₂) (hxy : x₁ = x₂y₁ W.negY x₂ y₂) :
                                W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

                                The addition of two nonsingular affine points in W on a sloped line is nonsingular.

                                theorem WeierstrassCurve.Affine.addX_eq_addX_negY_sub {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} (y₁ : F) (y₂ : F) (hx : x₁ x₂) :
                                W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) = W.addX x₁ x₂ (W.slope x₁ x₂ y₁ (W.negY x₂ y₂)) - (y₁ - W.negY x₁ y₁) * (y₂ - W.negY x₂ y₂) / (x₂ - x₁) ^ 2

                                The formula x(P₁ + P₂) = x(P₁ - P₂) - ψ(P₁)ψ(P₂) / (x(P₂) - x(P₁))², where ψ(x,y) = 2y + a₁x + a₃.

                                theorem WeierstrassCurve.Affine.cyclic_sum_Y_mul_X_sub_X {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} (y₁ : F) (y₂ : F) (hx : x₁ x₂) :
                                y₁ * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) + y₂ * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) + W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) * (x₁ - x₂) = 0

                                The formula y(P₁)(x(P₂) - x(P₃)) + y(P₂)(x(P₃) - x(P₁)) + y(P₃)(x(P₁) - x(P₂)) = 0, assuming that P₁ + P₂ + P₃ = O.

                                theorem WeierstrassCurve.Affine.addY_sub_negY_addY {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} (y₁ : F) (y₂ : F) (hx : x₁ x₂) :
                                W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂) - W.negY (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)) = ((y₂ - W.negY x₂ y₂) * (x₁ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) - (y₁ - W.negY x₁ y₁) * (x₂ - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) / (x₂ - x₁)

                                The formula ψ(P₁ + P₂) = (ψ(P₂)(x(P₁) - x(P₃)) - ψ(P₁)(x(P₂) - x(P₃))) / (x(P₂) - x(P₁)), where ψ(x,y) = 2y + a₁x + a₃.

                                Group operations #

                                A nonsingular rational point on a Weierstrass curve W in affine coordinates. This is either the unique point at infinity WeierstrassCurve.Affine.Point.zero or the nonsingular affine points WeierstrassCurve.Affine.Point.some $(x, y)$ satisfying the Weierstrass equation of W.

                                Instances For

                                  For an algebraic extension S of R, the type of nonsingular S-rational points on W.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    Pretty printer defined by notation3 command.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      Equations
                                      • WeierstrassCurve.Affine.Point.instInhabited = { default := WeierstrassCurve.Affine.Point.zero }
                                      Equations
                                      • WeierstrassCurve.Affine.Point.instZero = { zero := WeierstrassCurve.Affine.Point.zero }
                                      theorem WeierstrassCurve.Affine.Point.zero_def {R : Type u} [CommRing R] {W : WeierstrassCurve.Affine R} :
                                      WeierstrassCurve.Affine.Point.zero = 0
                                      def WeierstrassCurve.Affine.Point.neg {R : Type u} [CommRing R] {W : WeierstrassCurve.Affine R} :
                                      W.PointW.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.Affine.Point.instNeg = { neg := WeierstrassCurve.Affine.Point.neg }
                                        theorem WeierstrassCurve.Affine.Point.neg_def {R : Type u} [CommRing R] {W : WeierstrassCurve.Affine R} (P : W.Point) :
                                        P.neg = -P
                                        Equations
                                        noncomputable def WeierstrassCurve.Affine.Point.add {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} :
                                        W.PointW.PointW.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
                                          noncomputable instance WeierstrassCurve.Affine.Point.instAddPoint {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} :
                                          Add W.Point
                                          Equations
                                          • WeierstrassCurve.Affine.Point.instAddPoint = { add := WeierstrassCurve.Affine.Point.add }
                                          theorem WeierstrassCurve.Affine.Point.add_def {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} (P : W.Point) (Q : W.Point) :
                                          P.add Q = P + Q
                                          Equations
                                          @[simp]
                                          theorem WeierstrassCurve.Affine.Point.add_of_Y_eq {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} (hx : x₁ = x₂) (hy : y₁ = W.negY x₂ y₂) :
                                          @[simp]
                                          theorem WeierstrassCurve.Affine.Point.add_self_of_Y_eq {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {y₁ : F} {h₁ : W.Nonsingular x₁ y₁} (hy : y₁ = W.negY x₁ y₁) :
                                          @[simp]
                                          theorem WeierstrassCurve.Affine.Point.add_of_imp {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} (hxy : x₁ = x₂y₁ W.negY x₂ y₂) :
                                          @[simp]
                                          theorem WeierstrassCurve.Affine.Point.add_of_Y_ne {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} (hy : y₁ W.negY x₂ y₂) :
                                          theorem WeierstrassCurve.Affine.Point.add_of_Y_ne' {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} (hy : y₁ W.negY x₂ y₂) :
                                          @[simp]
                                          theorem WeierstrassCurve.Affine.Point.add_self_of_Y_ne {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {y₁ : F} {h₁ : W.Nonsingular x₁ y₁} (hy : y₁ W.negY x₁ y₁) :
                                          theorem WeierstrassCurve.Affine.Point.add_self_of_Y_ne' {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {y₁ : F} {h₁ : W.Nonsingular x₁ y₁} (hy : y₁ W.negY x₁ y₁) :
                                          @[simp]
                                          theorem WeierstrassCurve.Affine.Point.add_of_X_ne {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} (hx : x₁ x₂) :
                                          theorem WeierstrassCurve.Affine.Point.add_of_X_ne' {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} (hx : x₁ x₂) :
                                          @[deprecated WeierstrassCurve.Affine.Point.add_of_Y_eq]
                                          theorem WeierstrassCurve.Affine.Point.some_add_some_of_Yeq {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} (hx : x₁ = x₂) (hy : y₁ = W.negY x₂ y₂) :

                                          Alias of WeierstrassCurve.Affine.Point.add_of_Y_eq.

                                          @[deprecated WeierstrassCurve.Affine.Point.add_self_of_Y_eq]
                                          theorem WeierstrassCurve.Affine.Point.some_add_self_of_Yeq {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {y₁ : F} {h₁ : W.Nonsingular x₁ y₁} (hy : y₁ = W.negY x₁ y₁) :

                                          Alias of WeierstrassCurve.Affine.Point.add_self_of_Y_eq.

                                          @[deprecated WeierstrassCurve.Affine.Point.add_of_Y_ne]
                                          theorem WeierstrassCurve.Affine.Point.some_add_some_of_Yne {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} (hy : y₁ W.negY x₂ y₂) :

                                          Alias of WeierstrassCurve.Affine.Point.add_of_Y_ne.

                                          @[deprecated WeierstrassCurve.Affine.Point.add_of_Y_ne']
                                          theorem WeierstrassCurve.Affine.Point.some_add_some_of_Yne' {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} (hy : y₁ W.negY x₂ y₂) :

                                          Alias of WeierstrassCurve.Affine.Point.add_of_Y_ne'.

                                          @[deprecated WeierstrassCurve.Affine.Point.add_self_of_Y_ne]
                                          theorem WeierstrassCurve.Affine.Point.some_add_self_of_Yne {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {y₁ : F} {h₁ : W.Nonsingular x₁ y₁} (hy : y₁ W.negY x₁ y₁) :

                                          Alias of WeierstrassCurve.Affine.Point.add_self_of_Y_ne.

                                          @[deprecated WeierstrassCurve.Affine.Point.add_self_of_Y_ne']
                                          theorem WeierstrassCurve.Affine.Point.some_add_self_of_Yne' {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {y₁ : F} {h₁ : W.Nonsingular x₁ y₁} (hy : y₁ W.negY x₁ y₁) :

                                          Alias of WeierstrassCurve.Affine.Point.add_self_of_Y_ne'.

                                          @[deprecated WeierstrassCurve.Affine.Point.add_of_X_ne]
                                          theorem WeierstrassCurve.Affine.Point.some_add_some_of_Xne {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} (hx : x₁ x₂) :

                                          Alias of WeierstrassCurve.Affine.Point.add_of_X_ne.

                                          @[deprecated WeierstrassCurve.Affine.Point.add_of_X_ne']
                                          theorem WeierstrassCurve.Affine.Point.some_add_some_of_Xne' {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} {h₁ : W.Nonsingular x₁ y₁} {h₂ : W.Nonsingular x₂ y₂} (hx : x₁ x₂) :

                                          Alias of WeierstrassCurve.Affine.Point.add_of_X_ne'.

                                          Maps across ring homomorphisms #

                                          theorem WeierstrassCurve.Affine.map_polynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type v} [CommRing S] (f : R →+* S) :
                                          (WeierstrassCurve.map W f).toAffine.polynomial = Polynomial.map (Polynomial.mapRingHom f) W.polynomial
                                          theorem WeierstrassCurve.Affine.evalEval_baseChange_polynomial_X_Y {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) :
                                          Polynomial.evalEval (Polynomial.C Polynomial.X) Polynomial.X (WeierstrassCurve.baseChange W (Polynomial (Polynomial R))).toAffine.polynomial = W.polynomial
                                          theorem WeierstrassCurve.Affine.Equation.map {R : Type u} [CommRing R] {W : WeierstrassCurve.Affine R} {S : Type v} [CommRing S] (f : R →+* S) {x : R} {y : R} (h : W.Equation x y) :
                                          theorem WeierstrassCurve.Affine.map_equation {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type v} [CommRing S] {f : R →+* S} (hf : Function.Injective f) (x : R) (y : R) :
                                          (WeierstrassCurve.map W f).toAffine.Equation (f x) (f y) W.Equation x y
                                          theorem WeierstrassCurve.Affine.map_polynomialX {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type v} [CommRing S] (f : R →+* S) :
                                          (WeierstrassCurve.map W f).toAffine.polynomialX = Polynomial.map (Polynomial.mapRingHom f) W.polynomialX
                                          theorem WeierstrassCurve.Affine.map_polynomialY {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type v} [CommRing S] (f : R →+* S) :
                                          (WeierstrassCurve.map W f).toAffine.polynomialY = Polynomial.map (Polynomial.mapRingHom f) W.polynomialY
                                          theorem WeierstrassCurve.Affine.map_nonsingular {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type v} [CommRing S] {f : R →+* S} (hf : Function.Injective f) (x : R) (y : R) :
                                          (WeierstrassCurve.map W f).toAffine.Nonsingular (f x) (f y) W.Nonsingular x y
                                          theorem WeierstrassCurve.Affine.map_negPolynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type v} [CommRing S] (f : R →+* S) :
                                          (WeierstrassCurve.map W f).toAffine.negPolynomial = Polynomial.map (Polynomial.mapRingHom f) W.negPolynomial
                                          theorem WeierstrassCurve.Affine.map_negY {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type v} [CommRing S] (f : R →+* S) (x : R) (y : R) :
                                          (WeierstrassCurve.map W f).toAffine.negY (f x) (f y) = f (W.negY x y)
                                          theorem WeierstrassCurve.Affine.map_addPolynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type v} [CommRing S] (f : R →+* S) (x : R) (y : R) (L : R) :
                                          (WeierstrassCurve.map W f).toAffine.addPolynomial (f x) (f y) (f L) = Polynomial.map f (W.addPolynomial x y L)
                                          theorem WeierstrassCurve.Affine.map_addX {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type v} [CommRing S] (f : R →+* S) (x₁ : R) (x₂ : R) (L : R) :
                                          (WeierstrassCurve.map W f).toAffine.addX (f x₁) (f x₂) (f L) = f (W.addX x₁ x₂ L)
                                          theorem WeierstrassCurve.Affine.map_negAddY {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type v} [CommRing S] (f : R →+* S) (x₁ : R) (x₂ : R) (y₁ : R) (L : R) :
                                          (WeierstrassCurve.map W f).toAffine.negAddY (f x₁) (f x₂) (f y₁) (f L) = f (W.negAddY x₁ x₂ y₁ L)
                                          theorem WeierstrassCurve.Affine.map_addY {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type v} [CommRing S] (f : R →+* S) (x₁ : R) (x₂ : R) (y₁ : R) (L : R) :
                                          (WeierstrassCurve.map W f).toAffine.addY (f x₁) (f x₂) (f y₁) (f L) = f ((WeierstrassCurve.toAffine W).addY x₁ x₂ y₁ L)
                                          theorem WeierstrassCurve.Affine.map_slope {F : Type u} [Field F] (W : WeierstrassCurve.Affine F) {K : Type v} [Field K] (f : F →+* K) (x₁ : F) (x₂ : F) (y₁ : F) (y₂ : F) :
                                          (WeierstrassCurve.map W f).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f (W.slope x₁ x₂ y₁ y₂)

                                          Base changes across algebra homomorphisms #

                                          theorem WeierstrassCurve.Affine.baseChange_polynomial {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) :
                                          (WeierstrassCurve.baseChange W B).toAffine.polynomial = Polynomial.map (Polynomial.mapRingHom f) (WeierstrassCurve.baseChange W A).toAffine.polynomial
                                          theorem WeierstrassCurve.Affine.baseChange_equation {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (hf : Function.Injective f) (x : A) (y : A) :
                                          (WeierstrassCurve.baseChange W B).toAffine.Equation (f x) (f y) (WeierstrassCurve.baseChange W A).toAffine.Equation x y
                                          theorem WeierstrassCurve.Affine.baseChange_polynomialX {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) :
                                          (WeierstrassCurve.baseChange W B).toAffine.polynomialX = Polynomial.map (Polynomial.mapRingHom f) (WeierstrassCurve.baseChange W A).toAffine.polynomialX
                                          theorem WeierstrassCurve.Affine.baseChange_polynomialY {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) :
                                          (WeierstrassCurve.baseChange W B).toAffine.polynomialY = Polynomial.map (Polynomial.mapRingHom f) (WeierstrassCurve.baseChange W A).toAffine.polynomialY
                                          theorem WeierstrassCurve.Affine.baseChange_nonsingular {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] {f : A →ₐ[S] B} (hf : Function.Injective f) (x : A) (y : A) :
                                          (WeierstrassCurve.baseChange W B).toAffine.Nonsingular (f x) (f y) (WeierstrassCurve.baseChange W A).toAffine.Nonsingular x y
                                          theorem WeierstrassCurve.Affine.baseChange_negPolynomial {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) :
                                          (WeierstrassCurve.baseChange W B).toAffine.negPolynomial = Polynomial.map (Polynomial.mapRingHom f) (WeierstrassCurve.baseChange W A).toAffine.negPolynomial
                                          theorem WeierstrassCurve.Affine.baseChange_negY {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (x : A) (y : A) :
                                          (WeierstrassCurve.baseChange W B).toAffine.negY (f x) (f y) = f ((WeierstrassCurve.baseChange W A).toAffine.negY x y)
                                          theorem WeierstrassCurve.Affine.baseChange_addPolynomial {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (x : A) (y : A) (L : A) :
                                          (WeierstrassCurve.baseChange W B).toAffine.addPolynomial (f x) (f y) (f L) = Polynomial.map (↑f) ((WeierstrassCurve.baseChange W A).toAffine.addPolynomial x y L)
                                          theorem WeierstrassCurve.Affine.baseChange_addX {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (x₁ : A) (x₂ : A) (L : A) :
                                          (WeierstrassCurve.baseChange W B).toAffine.addX (f x₁) (f x₂) (f L) = f ((WeierstrassCurve.baseChange W A).toAffine.addX x₁ x₂ L)
                                          theorem WeierstrassCurve.Affine.baseChange_negAddY {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (x₁ : A) (x₂ : A) (y₁ : A) (L : A) :
                                          (WeierstrassCurve.baseChange W B).toAffine.negAddY (f x₁) (f x₂) (f y₁) (f L) = f ((WeierstrassCurve.baseChange W A).toAffine.negAddY x₁ x₂ y₁ L)
                                          theorem WeierstrassCurve.Affine.baseChange_addY {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (x₁ : A) (x₂ : A) (y₁ : A) (L : A) :
                                          (WeierstrassCurve.baseChange W B).toAffine.addY (f x₁) (f x₂) (f y₁) (f L) = f ((WeierstrassCurve.baseChange W A).toAffine.addY x₁ x₂ y₁ L)
                                          theorem WeierstrassCurve.Affine.baseChange_slope {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {F : Type u} [Field F] [Algebra R F] [Algebra S F] [IsScalarTower R S F] {K : Type v} [Field K] [Algebra R K] [Algebra S K] [IsScalarTower R S K] (f : F →ₐ[S] K) (x₁ : F) (x₂ : F) (y₁ : F) (y₂ : F) :
                                          (WeierstrassCurve.baseChange W K).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f ((WeierstrassCurve.baseChange W F).toAffine.slope x₁ x₂ y₁ y₂)

                                          The function from W⟮F⟯ to W⟮K⟯ induced by an algebra homomorphism f : F →ₐ[S] K, where W is defined over a subring of a ring S, and F and K are field extensions of S.

                                          Equations
                                          Instances For

                                            The group homomorphism from W⟮F⟯ to W⟮K⟯ induced by an algebra homomorphism f : F →ₐ[S] K, where W is defined over a subring of a ring S, and F and K are field extensions of S.

                                            Equations
                                            Instances For
                                              theorem WeierstrassCurve.Affine.Point.map_zero {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {F : Type u} [Field F] [Algebra R F] [Algebra S F] [IsScalarTower R S F] {K : Type v} [Field K] [Algebra R K] [Algebra S K] [IsScalarTower R S K] (f : F →ₐ[S] K) :
                                              theorem WeierstrassCurve.Affine.Point.map_some {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {F : Type u} [Field F] [Algebra R F] [Algebra S F] [IsScalarTower R S F] {K : Type v} [Field K] [Algebra R K] [Algebra S K] [IsScalarTower R S K] (f : F →ₐ[S] K) {x : F} {y : F} (h : (WeierstrassCurve.baseChange W F).toAffine.Nonsingular x y) :
                                              @[reducible, inline]

                                              The group homomorphism from W⟮F⟯ to W⟮K⟯ induced by the base change from F to K, where W is defined over a subring of a ring S, and F and K are field extensions of S.

                                              Equations
                                              Instances For
                                                @[deprecated WeierstrassCurve.Affine.negAddY]
                                                def WeierstrassCurve.Affine.addY' {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x₁ : R) (x₂ : R) (y₁ : R) (L : R) :
                                                R

                                                Alias of WeierstrassCurve.Affine.negAddY.


                                                The $Y$-coordinate of the negated addition of two affine points $(x_1, y_1)$ and $(x_2, y_2)$, where the line through them is not vertical and has a slope of $L$.

                                                This depends on W, and has argument order: $x_1$, $x_2$, $y_1$, $L$.

                                                Equations
                                                Instances For
                                                  @[deprecated WeierstrassCurve.Affine.nonsingular_negAdd_of_eval_derivative_ne_zero]
                                                  theorem WeierstrassCurve.Affine.nonsingular_add_of_eval_derivative_ne_zero {R : Type u} [CommRing R] {W : WeierstrassCurve.Affine R} {x₁ : R} {x₂ : R} {y₁ : R} {L : R} (hx' : W.Equation (W.addX x₁ x₂ L) (W.negAddY x₁ x₂ y₁ L)) (hx : Polynomial.eval (W.addX x₁ x₂ L) (Polynomial.derivative (W.addPolynomial x₁ y₁ L)) 0) :
                                                  W.Nonsingular (W.addX x₁ x₂ L) (W.negAddY x₁ x₂ y₁ L)

                                                  Alias of WeierstrassCurve.Affine.nonsingular_negAdd_of_eval_derivative_ne_zero.

                                                  @[deprecated WeierstrassCurve.Affine.slope_of_Y_eq]
                                                  theorem WeierstrassCurve.Affine.slope_of_Yeq {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (hx : x₁ = x₂) (hy : y₁ = W.negY x₂ y₂) :
                                                  W.slope x₁ x₂ y₁ y₂ = 0

                                                  Alias of WeierstrassCurve.Affine.slope_of_Y_eq.

                                                  @[deprecated WeierstrassCurve.Affine.slope_of_Y_ne]
                                                  theorem WeierstrassCurve.Affine.slope_of_Yne {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (hx : x₁ = x₂) (hy : y₁ W.negY x₂ y₂) :
                                                  W.slope x₁ x₂ y₁ y₂ = (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁)

                                                  Alias of WeierstrassCurve.Affine.slope_of_Y_ne.

                                                  @[deprecated WeierstrassCurve.Affine.slope_of_X_ne]
                                                  theorem WeierstrassCurve.Affine.slope_of_Xne {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (hx : x₁ x₂) :
                                                  W.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂)

                                                  Alias of WeierstrassCurve.Affine.slope_of_X_ne.

                                                  @[deprecated WeierstrassCurve.Affine.slope_of_Y_ne_eq_eval]
                                                  theorem WeierstrassCurve.Affine.slope_of_Yne_eq_eval {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (hx : x₁ = x₂) (hy : y₁ W.negY x₂ y₂) :
                                                  W.slope x₁ x₂ y₁ y₂ = -Polynomial.evalEval x₁ y₁ W.polynomialX / Polynomial.evalEval x₁ y₁ W.polynomialY

                                                  Alias of WeierstrassCurve.Affine.slope_of_Y_ne_eq_eval.

                                                  @[deprecated WeierstrassCurve.Affine.Y_eq_of_X_eq]
                                                  theorem WeierstrassCurve.Affine.Yeq_of_Xeq {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hx : x₁ = x₂) :
                                                  y₁ = y₂ y₁ = W.negY x₂ y₂

                                                  Alias of WeierstrassCurve.Affine.Y_eq_of_X_eq.

                                                  @[deprecated WeierstrassCurve.Affine.Y_eq_of_Y_ne]
                                                  theorem WeierstrassCurve.Affine.Yeq_of_Yne {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hx : x₁ = x₂) (hy : y₁ W.negY x₂ y₂) :
                                                  y₁ = y₂

                                                  Alias of WeierstrassCurve.Affine.Y_eq_of_Y_ne.

                                                  @[deprecated WeierstrassCurve.Affine.equation_negAdd]
                                                  theorem WeierstrassCurve.Affine.equation_add' {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hxy : x₁ = x₂y₁ W.negY x₂ y₂) :
                                                  W.Equation (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

                                                  Alias of WeierstrassCurve.Affine.equation_negAdd.


                                                  The negated addition of two affine points in W on a sloped line lies in W.

                                                  @[deprecated WeierstrassCurve.Affine.nonsingular_negAdd]
                                                  theorem WeierstrassCurve.Affine.nonsingular_add' {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : W.Nonsingular x₁ y₁) (h₂ : W.Nonsingular x₂ y₂) (hxy : x₁ = x₂y₁ W.negY x₂ y₂) :
                                                  W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))

                                                  Alias of WeierstrassCurve.Affine.nonsingular_negAdd.


                                                  The negated addition of two nonsingular affine points in W on a sloped line is nonsingular.

                                                  @[deprecated WeierstrassCurve.Affine.baseChange_negAddY]
                                                  theorem WeierstrassCurve.Affine.baseChange_addY' {R : Type r} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [CommRing S] [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (x₁ : A) (x₂ : A) (y₁ : A) (L : A) :
                                                  (WeierstrassCurve.baseChange W B).toAffine.negAddY (f x₁) (f x₂) (f y₁) (f L) = f ((WeierstrassCurve.baseChange W A).toAffine.negAddY x₁ x₂ y₁ L)

                                                  Alias of WeierstrassCurve.Affine.baseChange_negAddY.

                                                  @[deprecated WeierstrassCurve.Affine.map_negAddY]
                                                  theorem WeierstrassCurve.Affine.map_addY' {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) {S : Type v} [CommRing S] (f : R →+* S) (x₁ : R) (x₂ : R) (y₁ : R) (L : R) :
                                                  (WeierstrassCurve.map W f).toAffine.negAddY (f x₁) (f x₂) (f y₁) (f L) = f (W.negAddY x₁ x₂ y₁ L)

                                                  Alias of WeierstrassCurve.Affine.map_negAddY.

                                                  Elliptic curves #

                                                  @[reducible, inline]

                                                  The coercion from an elliptic curve to a Weierstrass curve in affine coordinates.

                                                  Equations
                                                  • E.toAffine = E.toAffine
                                                  Instances For
                                                    theorem EllipticCurve.Affine.nonsingular {R : Type u} [CommRing R] (E : EllipticCurve R) [Nontrivial R] {x : R} {y : R} (h : E.toAffine.Equation x y) :
                                                    E.toAffine.Nonsingular x y