equiv_some_of_Z_ne_zero — Mathlib

English

For P, Q with nonzero Z, the equality P_y Q_z^3 = Q_y P_z^3 is equivalent to P_y/P_z^3 = Q_y/Q_z^3.

Русский

Для точек P, Q с ненулевой Z-координатой равенство P_y Q_z^3 = Q_y P_z^3 эквивалентно P_y/P_z^3 = Q_y/Q_z^3.

LaTeX

$$P_y Q_z^3 = Q_y P_z^3 iff P_y/P_z^3 = Q_y/Q_z^3$$

Lean4

theorem equiv_some_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) : P ≈ ![P x / P z ^ 2, P y / P z ^ 3, 1] :=
  equiv_of_X_eq_of_Y_eq hPz one_ne_zero
    (by linear_combination (norm := (matrix_simp; ring1)) -P x * div_self (pow_ne_zero 2 hPz))
    (by linear_combination (norm := (matrix_simp; ring1)) -P y * div_self (pow_ne_zero 3 hPz))

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