dblU_eq

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.Jacobian.dblU_eq

← MathLib Explorer

English

For any P and scalar u, W'.dblU (u • P) = u^4 W'.dblU P.

Русский

Для любого P и скаляра u выполняется W'.dblU (u • P) = u^4 W'.dblU P.

LaTeX

$$$W'.dblU (u \cdot P) = u^4 \cdot W'.dblU P$$$

Lean4

theorem dblU_eq (P : Fin 3 → R) :
    W'.dblU P = W'.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W'.a₂ * P x * P z ^ 2 + W'.a₄ * P z ^ 4) := by
  rw [dblU, eval_polynomialX]

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

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

Разделы

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

Аффилиация

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