negY_smul

Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

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

English

If Z = 0, then negY reduces to -Y.

Русский

Если Z = 0, то negY равно -Y.

LaTeX

$$$$ W'.negY(P) = -P_y $$ при P_z = 0$$

Lean4

theorem negY_smul (P : Fin 3 → R) (u : R) : W'.negY (u • P) = u ^ 3 * W'.negY P :=
  by
  simp only [negY, smul_fin3_ext]
  ring1

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

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

Разделы

Аффилиация

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