addXYZ_neg — Mathlib

English

Let W' be a projective Weierstrass curve over a commutative ring R, and P : Fin 3 → R with P on W'. Then the three-coordinate addition with the negation of P yields the Z-coordinate times the vector [0,1,0], namely W'.addXYZ P (W'.neg P) = -W'.dblZ P • ![0,1,0].

Русский

Пусть W' — проективная кривая Вейерштрасса над R, и P ∈ R^3 лежит на W'. Тогда тройная система сложения с отрицанием P дает вектор вдоль z-координаты: W'.addXYZ P (W'.neg P) = -W'.dblZ P • ![0,1,0].

LaTeX

$$$ W'.addXYZ P (W'.neg P) = -W'.dblZ P \\cdot ![0,1,0] $$$

Lean4

theorem addXYZ_neg {P : Fin 3 → R} (hP : W'.Equation P) : W'.addXYZ P (W'.neg P) = -W'.dblZ P • ![0, 1, 0] := by
  erw [addXYZ, addX_neg, addY_neg hP, addZ_neg, smul_fin3, mul_zero, mul_one]

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