dblU_smul

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.Projective.dblU_smul

English

dblZ P equals P_z (P_y − negY P)^3.

Русский

dblZ P равно P_z (P_y − negY P)^3.

LaTeX

$$$ W'.dblZ P = P_z \\left(P_y - W'.negY P\\right)^3 $$$

Lean4

theorem dblU_smul (P : Fin 3 → F) (u : F) : W.dblU (u • P) = u ^ 4 * W.dblU P := by simp [field, dblU_eq]

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

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

Разделы

Аффилиация

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