addY_neg — Mathlib

English

Let W' be a projective Weierstrass curve defined over a commutative ring R, and P : Fin 3 → R a triple lying on W'. Then the Y-coordinate addition with the negation of P satisfies W'.addY P (W'.neg P) = - W'.dblZ P.

Русский

Пусть W' — проективная кривая Вейерштрасса над коммутативной кольцом R, и P : Fin 3 → R тройка такая, что P лежит на W'. Тогда сумма по координате y с отрицанием P равна − dblZ P: W'.addY P (W'.neg P) = − W'.dblZ P.

LaTeX

$$$ W'.addY P (W'.neg P) = - W'.dblZ P $$$

Lean4

theorem addY_neg {P : Fin 3 → R} (hP : W'.Equation P) : W'.addY P (W'.neg P) = -W'.dblZ P := by
  simp only [addY, addX_neg, negAddY_neg hP, addZ_neg, negY, fin3_def_ext, mul_zero, sub_zero]

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