Negation and addition formulae for nonsingular points in affine coordinates

Let W be a Weierstrass curve over a field F with coefficients aᵢ. The nonsingular affine points on W can be given negation and addition operations defined by a secant-and-tangent process.

• Given a nonsingular affine point P, its negation -P is defined to be the unique third nonsingular point of intersection between W and the vertical line through P. Explicitly, if P is (x, y), then -P is (x, -y - a₁x - a₃).

• Given two nonsingular affine points P and Q, their addition P + Q is defined to be the negation of the unique third nonsingular point of intersection between W and the line L through P and Q. Explicitly, let P be (x₁, y₁) and let Q be (x₂, y₂).

  • If x₁ = x₂ and y₁ = -y₂ - a₁x₂ - a₃, then L is vertical.
  • If x₁ = x₂ and y₁ ≠ -y₂ - a₁x₂ - a₃, then L is the tangent of W at P = Q, and has slope ℓ := (3x₁² + 2a₂x₁ + a₄ - a₁y₁) / (2y₁ + a₁x₁ + a₃).
  • Otherwise x₁ ≠ x₂, then L is the secant of W through P and Q, and has slope ℓ := (y₁ - y₂) / (x₁ - x₂).

  In the last two cases, the X-coordinate of P + Q is then the unique third solution of the equation obtained by substituting the line Y = ℓ(X - x₁) + y₁ into the Weierstrass equation, and can be written down explicitly as x := ℓ² + a₁ℓ - a₂ - x₁ - x₂ by inspecting the coefficients of X². The Y-coordinate of P + Q, after applying the final negation that maps Y to -Y - a₁X - a₃, is precisely y := -(ℓ(x - x₁) + y₁) - a₁x - a₃.

This file defines polynomials associated to negation and addition of nonsingular affine points, including slopes of non-vertical lines. The actual group law on nonsingular points in affine coordinates will be defined in Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean.

Main definitions

• WeierstrassCurve.Affine.negY: the Y-coordinate of -P.
• WeierstrassCurve.Affine.addX: the X-coordinate of P + Q.
• WeierstrassCurve.Affine.negAddY: the Y-coordinate of -(P + Q).
• WeierstrassCurve.Affine.addY: the Y-coordinate of P + Q.

Main statements

• WeierstrassCurve.Affine.equation_neg: negation preserves the Weierstrass equation.
• WeierstrassCurve.Affine.nonsingular_neg: negation preserves the nonsingular condition.
• WeierstrassCurve.Affine.equation_add: addition preserves the Weierstrass equation.
• WeierstrassCurve.Affine.nonsingular_add: addition preserves the nonsingular condition.

References

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

Tags

elliptic curve, affine, negation, doubling, addition, group law

Negation formulae in affine coordinates

noncomputable def WeierstrassCurve.Affine.negPolynomial {R : Type r} [CommRing R] (W' : Affine R) : Polynomial (Polynomial R)

The negation polynomial -Y - a₁X - a₃ associated to the negation of a nonsingular affine point on a Weierstrass curve.

Equations

• W'.negPolynomial = -Polynomial.X - Polynomial.C (Polynomial.C W'.a₁ * Polynomial.X + Polynomial.C W'.a₃)

theorem WeierstrassCurve.Affine.Y_sub_polynomialY {R : Type r} [CommRing R] {W' : Affine R} : Polynomial.X - W'.polynomialY = W'.negPolynomial

theorem WeierstrassCurve.Affine.Y_sub_negPolynomial {R : Type r} [CommRing R] {W' : Affine R} : Polynomial.X - W'.negPolynomial = W'.polynomialY

def WeierstrassCurve.Affine.negY {R : Type r} [CommRing R] (W' : Affine R) (x y : R) : R

The Y-coordinate of -(x, y) for a nonsingular affine point (x, y) on a Weierstrass curve W.

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

Equations

• W'.negY x y = -y - W'.a₁ * x - W'.a₃

theorem WeierstrassCurve.Affine.negY_negY {R : Type r} [CommRing R] {W' : Affine R} (x y : R) : W'.negY x (W'.negY x y) = y

theorem WeierstrassCurve.Affine.evalEval_negPolynomial {R : Type r} [CommRing R] {W' : Affine R} (x y : R) : Polynomial.evalEval x y W'.negPolynomial = W'.negY x y

@[deprecated WeierstrassCurve.Affine.evalEval_negPolynomial (since := "2025-03-05")]

theorem WeierstrassCurve.Affine.eval_negPolynomial {R : Type r} [CommRing R] {W' : Affine R} (x y : R) : Polynomial.evalEval x y W'.negPolynomial = W'.negY x y

Alias of WeierstrassCurve.Affine.evalEval_negPolynomial.

theorem WeierstrassCurve.Affine.Y_eq_of_X_eq {F : Type u} [Field F] {W : Affine F} {x₁ x₂ y₁ 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 : Affine F} {x₁ x₂ y₁ 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.equation_neg {R : Type r} [CommRing R] {W' : Affine R} (x y : R) : W'.Equation x (W'.negY x y) ↔ W'.Equation x y

@[deprecated WeierstrassCurve.Affine.equation_neg (since := "2025-02-01")]

theorem WeierstrassCurve.Affine.equation_neg_of {R : Type r} [CommRing R] {W' : Affine R} (x y : R) : W'.Equation x (W'.negY x y) ↔ W'.Equation x y

Alias of WeierstrassCurve.Affine.equation_neg.

@[deprecated WeierstrassCurve.Affine.equation_neg (since := "2025-02-01")]

theorem WeierstrassCurve.Affine.equation_neg_iff {R : Type r} [CommRing R] {W' : Affine R} (x y : R) : W'.Equation x (W'.negY x y) ↔ W'.Equation x y

Alias of WeierstrassCurve.Affine.equation_neg.

theorem WeierstrassCurve.Affine.nonsingular_neg {R : Type r} [CommRing R] {W' : Affine R} (x y : R) : W'.Nonsingular x (W'.negY x y) ↔ W'.Nonsingular x y

@[deprecated WeierstrassCurve.Affine.nonsingular_neg (since := "2025-02-01")]

theorem WeierstrassCurve.Affine.nonsingular_neg_of {R : Type r} [CommRing R] {W' : Affine R} (x y : R) : W'.Nonsingular x (W'.negY x y) ↔ W'.Nonsingular x y

Alias of WeierstrassCurve.Affine.nonsingular_neg.

@[deprecated WeierstrassCurve.Affine.nonsingular_neg (since := "2025-02-01")]

theorem WeierstrassCurve.Affine.nonsingular_neg_iff {R : Type r} [CommRing R] {W' : Affine R} (x y : R) : W'.Nonsingular x (W'.negY x y) ↔ W'.Nonsingular x y

Alias of WeierstrassCurve.Affine.nonsingular_neg.

Slope formulae in affine coordinates

noncomputable def WeierstrassCurve.Affine.linePolynomial {R : Type r} [CommRing R] (x y ℓ : R) : Polynomial R

The line polynomial ℓ(X - x) + y associated to the line Y = ℓ(X - x) + y that passes through a nonsingular affine point (x, y) on a Weierstrass curve W with a slope of ℓ.

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

Equations

• WeierstrassCurve.Affine.linePolynomial x y ℓ = Polynomial.C ℓ * (Polynomial.X - Polynomial.C x) + Polynomial.C y

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

The slope of the line through two nonsingular affine points (x₁, y₁) and (x₂, y₂) on a Weierstrass curve W.

If x₁ ≠ x₂, then this line is the secant of W through (x₁, y₁) and (x₂, y₂), and has slope (y₁ - y₂) / (x₁ - x₂). Otherwise, if y₁ ≠ -y₁ - a₁x₁ - a₃, then this line is the tangent of W at (x₁, y₁) = (x₂, y₂), and has slope (3x₁² + 2a₂x₁ + a₄ - a₁y₁) / (2y₁ + a₁x₁ + a₃). Otherwise, this line is vertical, in which case this returns the value 0.

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

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₂)

@[simp]

theorem WeierstrassCurve.Affine.slope_of_Y_eq {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ 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 : Affine F} [DecidableEq F] {x₂ y₁ y₂ : F} (hy : ¬y₁ = -y₂ - W.a₁ * x₂ - W.a₃) : W.slope x₂ x₂ y₁ y₂ = (3 * x₂ ^ 2 + 2 * W.a₂ * x₂ + W.a₄ - W.a₁ * y₁) / (y₁ - (-y₁ - W.a₁ * x₂ - W.a₃))

theorem WeierstrassCurve.Affine.slope_of_Y_ne {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ 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 : Affine F} [DecidableEq F] {x₁ x₂ y₁ y₂ : F} (hx : x₁ ≠ x₂) : W.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂)

theorem WeierstrassCurve.Affine.slope_of_Y_ne_eq_evalEval {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ 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

@[deprecated WeierstrassCurve.Affine.slope_of_Y_ne_eq_evalEval (since := "2025-03-05")]

theorem WeierstrassCurve.Affine.slope_of_Y_ne_eq_eval {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ 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_evalEval.

Addition formulae in affine coordinates

noncomputable def WeierstrassCurve.Affine.addPolynomial {R : Type r} [CommRing R] (W' : Affine R) (x y ℓ : R) : Polynomial R

The addition polynomial obtained by substituting the line Y = ℓ(X - x) + y into the polynomial W(X, Y) associated to a Weierstrass curve W. If such a line intersects W at another nonsingular affine point (x', y') on W, 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, ℓ.

Equations

• W'.addPolynomial x y ℓ = Polynomial.eval (WeierstrassCurve.Affine.linePolynomial x y ℓ) W'.polynomial

theorem WeierstrassCurve.Affine.C_addPolynomial {R : Type r} [CommRing R] {W' : Affine R} (x y ℓ : R) : Polynomial.C (W'.addPolynomial x y ℓ) = (Polynomial.X - Polynomial.C (linePolynomial x y ℓ)) * (W'.negPolynomial - Polynomial.C (linePolynomial x y ℓ)) + W'.polynomial

theorem WeierstrassCurve.Affine.addPolynomial_eq {R : Type r} [CommRing R] {W' : Affine R} (x y ℓ : R) : W'.addPolynomial x y ℓ = -{ a := 1, b := -ℓ ^ 2 - W'.a₁ * ℓ + W'.a₂, c := 2 * x * ℓ ^ 2 + (W'.a₁ * x - 2 * y - W'.a₃) * ℓ + (-W'.a₁ * y + W'.a₄), d := -x ^ 2 * ℓ ^ 2 + (2 * x * y + W'.a₃ * x) * ℓ - (y ^ 2 + W'.a₃ * y - W'.a₆) }.toPoly

def WeierstrassCurve.Affine.addX {R : Type r} [CommRing R] (W' : Affine R) (x₁ x₂ ℓ : R) : R

The X-coordinate of (x₁, y₁) + (x₂, y₂) for two nonsingular affine points (x₁, y₁) and (x₂, y₂) on a Weierstrass curve W, where the line through them has a slope of ℓ.

This depends on W, and has argument order: x₁, x₂, ℓ.

Equations

• W'.addX x₁ x₂ ℓ = ℓ ^ 2 + W'.a₁ * ℓ - W'.a₂ - x₁ - x₂

def WeierstrassCurve.Affine.negAddY {R : Type r} [CommRing R] (W' : Affine R) (x₁ x₂ y₁ ℓ : R) : R

The Y-coordinate of -((x₁, y₁) + (x₂, y₂)) for two nonsingular affine points (x₁, y₁) and (x₂, y₂) on a Weierstrass curve W, where the line through them has a slope of ℓ.

This depends on W, and has argument order: x₁, x₂, y₁, ℓ.

Equations

• W'.negAddY x₁ x₂ y₁ ℓ = ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁

def WeierstrassCurve.Affine.addY {R : Type r} [CommRing R] (W' : Affine R) (x₁ x₂ y₁ ℓ : R) : R

The Y-coordinate of (x₁, y₁) + (x₂, y₂) for two nonsingular affine points (x₁, y₁) and (x₂, y₂) on a Weierstrass curve W, where the line through them has a slope of ℓ.

This depends on W, and has argument order: x₁, x₂, y₁, ℓ.

Equations

• W'.addY x₁ x₂ y₁ ℓ = W'.negY (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)

theorem WeierstrassCurve.Affine.addPolynomial_slope {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ 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.C_addPolynomial_slope {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) : Polynomial.C (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) = -(Polynomial.C (Polynomial.X - Polynomial.C x₁) * Polynomial.C (Polynomial.X - Polynomial.C x₂) * Polynomial.C (Polynomial.X - Polynomial.C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))

theorem WeierstrassCurve.Affine.derivative_addPolynomial_slope {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ 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_of_eval_derivative_ne_zero {R : Type r} [CommRing R] {W' : Affine R} {x₁ x₂ y₁ ℓ : R} (hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)) (hx : Polynomial.eval (W'.addX x₁ x₂ ℓ) (Polynomial.derivative (W'.addPolynomial x₁ y₁ ℓ)) ≠ 0) : W'.Nonsingular (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)

theorem WeierstrassCurve.Affine.equation_add_iff {R : Type r} [CommRing R] {W' : Affine R} (x₁ x₂ y₁ ℓ : R) : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ) ↔ Polynomial.eval (W'.addX x₁ x₂ ℓ) (W'.addPolynomial x₁ y₁ ℓ) = 0

theorem WeierstrassCurve.Affine.equation_negAdd {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ 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₂))

theorem WeierstrassCurve.Affine.equation_add {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ 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₂))

theorem WeierstrassCurve.Affine.nonsingular_negAdd {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ 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₂))

theorem WeierstrassCurve.Affine.nonsingular_add {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ y₁ 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₂))

theorem WeierstrassCurve.Affine.addX_eq_addX_negY_sub {F : Type u} [Field F] {W : Affine F} [DecidableEq F] {x₁ x₂ : F} (y₁ 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 : Affine F} [DecidableEq F] {x₁ x₂ : F} (y₁ y₂ : F) (hx : x₁ ≠ x₂) : have x₃ := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂); y₁ * (x₂ - x₃) + y₂ * (x₃ - 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 : Affine F} [DecidableEq F] {x₁ x₂ : F} (y₁ y₂ : F) (hx : x₁ ≠ x₂) : have x₃ := W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂); have y₃ := W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂); y₃ - W.negY x₃ y₃ = ((y₂ - W.negY x₂ y₂) * (x₁ - x₃) - (y₁ - W.negY x₁ y₁) * (x₂ - x₃)) / (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₃.

Maps and base changes

theorem WeierstrassCurve.Affine.map_negPolynomial {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} (f : R →+* S) : (map W' f).toAffine.negPolynomial = Polynomial.map (Polynomial.mapRingHom f) W'.negPolynomial

theorem WeierstrassCurve.Affine.map_negY {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} (f : R →+* S) (x y : R) : (map W' f).toAffine.negY (f x) (f y) = f (W'.negY x y)

theorem WeierstrassCurve.Affine.map_linePolynomial {R : Type r} {S : Type s} [CommRing R] [CommRing S] (f : R →+* S) (x y ℓ : R) : linePolynomial (f x) (f y) (f ℓ) = Polynomial.map f (linePolynomial x y ℓ)

theorem WeierstrassCurve.Affine.map_addPolynomial {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} (f : R →+* S) (x y ℓ : R) : (map W' f).toAffine.addPolynomial (f x) (f y) (f ℓ) = Polynomial.map f (W'.addPolynomial x y ℓ)

theorem WeierstrassCurve.Affine.map_addX {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} (f : R →+* S) (x₁ x₂ ℓ : R) : (map W' f).toAffine.addX (f x₁) (f x₂) (f ℓ) = f (W'.addX x₁ x₂ ℓ)

theorem WeierstrassCurve.Affine.map_negAddY {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} (f : R →+* S) (x₁ y₁ x₂ ℓ : R) : (map W' f).toAffine.negAddY (f x₁) (f x₂) (f y₁) (f ℓ) = f (W'.negAddY x₁ x₂ y₁ ℓ)

theorem WeierstrassCurve.Affine.map_addY {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Affine R} (f : R →+* S) (x₁ y₁ x₂ ℓ : R) : (map W' f).toAffine.addY (f x₁) (f x₂) (f y₁) (f ℓ) = f ((toAffine W').addY x₁ x₂ y₁ ℓ)

theorem WeierstrassCurve.Affine.map_slope {F : Type u} {K : Type v} [Field F] [Field K] {W : Affine F} [DecidableEq F] [DecidableEq K] (f : F →+* K) (x₁ x₂ y₁ y₂ : F) : (map W f).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f (W.slope x₁ x₂ y₁ y₂)

theorem WeierstrassCurve.Affine.baseChange_negPolynomial {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Affine R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) : (baseChange W' B).toAffine.negPolynomial = Polynomial.map (Polynomial.mapRingHom ↑f) (baseChange W' A).toAffine.negPolynomial

theorem WeierstrassCurve.Affine.baseChange_negY {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Affine R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (x y : A) : (baseChange W' B).toAffine.negY (f x) (f y) = f ((baseChange W' A).toAffine.negY x y)

theorem WeierstrassCurve.Affine.baseChange_addPolynomial {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Affine R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (x y ℓ : A) : (baseChange W' B).toAffine.addPolynomial (f x) (f y) (f ℓ) = Polynomial.map (↑f) ((baseChange W' A).toAffine.addPolynomial x y ℓ)

theorem WeierstrassCurve.Affine.baseChange_addX {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Affine R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (x₁ x₂ ℓ : A) : (baseChange W' B).toAffine.addX (f x₁) (f x₂) (f ℓ) = f ((baseChange W' A).toAffine.addX x₁ x₂ ℓ)

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

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

theorem WeierstrassCurve.Affine.baseChange_slope {R : Type r} {S : Type s} {F : Type u} {K : Type v} [CommRing R] [CommRing S] [Field F] [Field K] {W' : Affine R} [Algebra R S] [DecidableEq F] [DecidableEq K] [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebra R K] [Algebra S K] [IsScalarTower R S K] (f : F →ₐ[S] K) (x₁ x₂ y₁ y₂ : F) : (baseChange W' K).toAffine.slope (f x₁) (f x₂) (f y₁) (f y₂) = f ((baseChange W' F).toAffine.slope x₁ x₂ y₁ y₂)