equiv_of_X_eq_of_Y_eq — Mathlib

English

If P z ≠ 0, then P is equivalent to the canonical representative with z=1, obtained by dividing coordinates by suitable powers of z.

Русский

Если P_z ≠ 0, то P эквивалентно каноническому представителю с z=1, полученному делением координат на соответствующие степени z.

LaTeX

$$If $P_z\neq 0$, then $P \approx \![P_x/P_z^2, P_y/P_z^3, 1]$$$

Lean4

theorem equiv_of_X_eq_of_Y_eq {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 = Q x * P z ^ 2)
    (hy : P y * Q z ^ 3 = Q y * P z ^ 3) : P ≈ Q :=
  by
  use Units.mk0 _ hPz / Units.mk0 _ hQz
  simp only [Units.smul_def, smul_fin3, Units.val_div_eq_div_val, Units.val_mk0, div_pow, mul_comm, mul_div, ← hx, ← hy,
    mul_div_cancel_right₀ _ <| pow_ne_zero _ hQz, mul_div_cancel_right₀ _ hQz, fin3_def]

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