equation_of_Z_ne_zero — Mathlib

English

If P z ≠ 0, then W'.Equation P is equivalent to the affine equation after changing variables x' = Px/Pz^2, y' = Py/Pz^3, using the affine slope.

Русский

Если Pz ≠ 0, то P удовлетворяет W'.Equation эквивалентно аффинному уравнению после замены переменных x' = Px/Pz^2, y' = Py/Pz^3 с использованием наклона аффинной кривой.

LaTeX

$$$W'.Equation(P) \\iff W'.toAffine.Equation\\left(\\frac{P_x}{P_z^2},\\frac{P_y}{P_z^3}\\right) \\text{ with slope as appropriate}$$$

Lean4

theorem equation_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
    W.Equation P ↔ W.toAffine.Equation (P x / P z ^ 2) (P y / P z ^ 3) :=
  (equation_of_equiv <| equiv_some_of_Z_ne_zero hPz).trans <| equation_some ..

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