isUnit_dblZ_of_Y_ne — Mathlib

English

Under NoZeroDivisors, if P and Q satisfy W.Equation for both and P z, Q z ≠ 0 with hx, hy, hy' giving proportionality constraints, then W.dblZ P is a unit in the base field, i.e., is invertible: IsUnit(W.dblZ P).

Русский

При NoZeroDivisors, если P и Q удовлетворяют равенствам на кривой, и P z, Q z ≠ 0 с условиями hx, hy, hy', то dblZ P является обратимым элементом: IsUnit(W.dblZ P).

LaTeX

$$$ [NoZeroDivisors\ R] \; {P,Q: \mathrm{Fin}(3)→R},\; W'.Equation P, W'.Equation Q,\; P_z ≠ 0, Q_z ≠ 0,\; 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 ≠ Q y * P z) : IsUnit (W.dblZ P) :=
  (dblZ_ne_zero_of_Y_ne hP hQ hPz hQz hx hy).isUnit

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