negPolynomial

Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

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

Lean4

/-- The negation polynomial `-Y - a₁X - a₃` associated to the negation of a nonsingular affine point
on a Weierstrass curve. -/
noncomputable def negPolynomial : R[X][Y] :=
  -(Y : R[X][Y]) - C (C W'.a₁ * X + C W'.a₃)

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

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

Разделы

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

Аффилиация

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