isUnit_dblZ_of_Y_ne' — Mathlib

English

Under NoZeroDivisors, with P,Q satisfying W'.Equation and the Y-relations including hy’, the Z-coordinate of 2P is a unit in the target field: IsUnit(W'.dblZ P).

Русский

При NoZeroDivisors, если P,Q удовлетворяют W'.Equation и соотношениям по Y, включая hy', Z-координата удвоенной точки единична: IsUnit(W'.dblZ P).

LaTeX

$$$ [NoZeroDivisors\ R] \; {P,Q}: \mathrm{Fin}(3)→R,\; hP,hQ, hPz,hQz, hx, hy, hy' \Rightarrow IsUnit(W'.dblZ P)$$$

Lean4

theorem isUnit_dblZ_of_Y_ne' {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
    (hx : P x * Q z = Q x * P z) (hy : P y * Q z ≠ W.negY Q * P z) : IsUnit (W.dblZ P) :=
  (dblZ_ne_zero_of_Y_ne' hP hQ hPz hQz hx hy).isUnit

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