equiv_some_of_Z_ne_zero — Mathlib

English

Given a valid P ≈ Q, the same cross-relations hold for X and Y components.

Русский

При допустимой эквивалентности P ≈ Q выполняются те же перекрестные отношения для X и Y.

LaTeX

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

Lean4

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

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