Theorems · Definition · algebraic geometry

WeierstrassCurve.Affine.slope

{F : Type u} → [Field F] → WeierstrassCurve.Affine F → [DecidableEq F] → F → F → F → 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₂.

Defined in

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Cited by

54 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Quot.sound

Assumes

FieldDecidableEq