dblY_smul — Mathlib

English

Under the Weierstrass framework, if P and Q satisfy the Y-relations, then W'.dblY P equals a cubic expression in P’s coordinates, scaled appropriately by P z.

Русский

В рамках кривой Вейерштрасса, если P и Q удовлетворяют Y-отношениям, то W'.dblY P выражается через кубическое выражение от координат P, масштабированное по P z.

LaTeX

$$$ {P Q: Fin 3→F} (hP: W'.Equation P) (hQ: W'.Equation Q) (hPz: P z ≠ 0) (hQz: Q z ≠ 0) (hy: P y Q z = Q y P z) (hy': P y Q z = W'.negY Q P z) : W'.dblY P = \frac{Eval(P) }{P z^4}$$$

Lean4

theorem dblY_smul (P : Fin 3 → R) (u : R) : W'.dblY (u • P) = u ^ 4 * W'.dblY P :=
  by
  simp only [dblY, negY_eq, negDblY_smul, dblX_smul, dblZ_smul]
  ring1

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