Y_eq_iff — Mathlib

English

Given nonzero Z and X, Y relations as above, there is a direct equivalence between P and Q in the Jacobian sense.

Русский

При ненулевых Z и соответствующих X, Y соотношениях существует прямая эквивалентность между P и Q в смысле эквивелентности Жакобиана.

LaTeX

$$If $P_z,Q_z\neq 0$, $P_xQ_z^2=Q_xP_z^2$, and $P_yQ_z^3=Q_yP_z^3$, then $P\approx Q$$$

Lean4

theorem Y_eq_iff {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0) :
    P y * Q z ^ 3 = Q y * P z ^ 3 ↔ P y / P z ^ 3 = Q y / Q z ^ 3 :=
  (div_eq_div_iff (pow_ne_zero 3 hPz) (pow_ne_zero 3 hQz)).symm

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