equiv_of_Z_eq_zero — Mathlib

English

If W is nonsingular at P and Q, and both have zero Z-coordinate, then P and Q are projectively equivalent (P ≈ Q).

Русский

Если W несингулярна в P и Q и обе тройки имеют Z=0, тогда P и Q эквивалентны по проективной эквивалентности (P ≈ Q).

LaTeX

$$$W.Nonsingular P \\land W.Nonsingular Q \\land P_z=0 \\land Q_z=0 \\Rightarrow P \\approx Q$$$

Lean4

theorem equiv_of_Z_eq_zero {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) (hPz : P z = 0)
    (hQz : Q z = 0) : P ≈ Q :=
  by
  use (isUnit_Y_of_Z_eq_zero hP hPz).unit / (isUnit_Y_of_Z_eq_zero hQ hQz).unit
  simp only [Units.smul_def, smul_fin3, X_eq_zero_of_Z_eq_zero hQ.left hQz, hQz, mul_zero, Units.val_div_eq_div_val,
    IsUnit.unit_spec, (isUnit_Y_of_Z_eq_zero hQ hQz).div_mul_cancel]
  conv_rhs => rw [← fin3_def P, X_eq_zero_of_Z_eq_zero hP.left hPz, hPz]

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