equation_iff — Mathlib

English

Let P be a 3-tuple over R and Q be another triple such that P ≈ Q (they represent the same projective point). Then P lies on the Weierstrass curve W' if and only if Q does as well.

Русский

Пусть P и Q — тройки над R и P ≈ Q (они представляют одну и ту же точку в проективном пространстве). Тогда P удовлетворяет уравнение кривой Вейерштрасса W' тогда и только тогда, когда и Q удовлетворяет его.

LaTeX

$$$\\forall P,Q:\\ Fin(3)\\to R,\\; P \\approx Q \\Rightarrow (W'.Equation(P) \\iff W'.Equation(Q))$$$

Lean4

theorem equation_iff (P : Fin 3 → R) :
    W'.Equation P ↔
      P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
          (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6) =
        0 :=
  by rw [Equation, eval_polynomial]

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