linePolynomial

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.Affine.linePolynomial

Lean4

/-- 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`, `ℓ`. -/
noncomputable def linePolynomial (x y ℓ : R) : R[X] :=
  C ℓ * (X - C x) + C y

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru