equiv_of_X_eq_of_Y_eq — Mathlib

English

For P,Q with Z-components nonzero, P ≈ Q implies X and Y ratios equal in the usual sense.

Русский

Для P,Q с ненулевыми Z-компонентами, P ≈ Q подразумевает равенство соответствующих отношений X и Y.

LaTeX

$$P x / P z = Q x / Q z ∧ P y / P z = Q y / Q z$$

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 = Q x * P z)
    (hy : P y * Q z = Q y * P z) : 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, mul_comm, mul_div, ← hx, ← hy,
    mul_div_cancel_right₀ _ hQz, fin3_def]

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