English
If P z = 0 and W.Nonsingular P, then P ≈ ![1,1,0].
Русский
Если P z = 0 и W неособая, то P эквивалентно ![1,1,0].
LaTeX
$$$ W.Nonsingular P \\Rightarrow P \\approx ![1,1,0] $$$
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
have hPx : IsUnit <| P x := isUnit_X_of_Z_eq_zero hP hPz
have hPy : IsUnit <| P y := isUnit_Y_of_Z_eq_zero hP hPz
have hQx : IsUnit <| Q x := isUnit_X_of_Z_eq_zero hQ hQz
have hQy : IsUnit <| Q y := isUnit_Y_of_Z_eq_zero hQ hQz
simp only [nonsingular_of_Z_eq_zero, equation_of_Z_eq_zero, hPz, hQz] at hP hQ
use (hPy.unit / hPx.unit) * (hQx.unit / hQy.unit)
simp only [Units.smul_def, smul_fin3, Units.val_mul, Units.val_div_eq_div_val, IsUnit.unit_spec, mul_pow, div_pow,
hQz, mul_zero]
conv_rhs => rw [← fin3_def P, hPz]
congr! 2
·
rw [hP.left, pow_succ, (hPx.pow 2).mul_div_cancel_left, hQ.left, pow_succ _ 2, (hQx.pow 2).div_mul_cancel_left,
hQx.inv_mul_cancel_right]
·
rw [← hP.left, pow_succ, (hPy.pow 2).mul_div_cancel_left, ← hQ.left, pow_succ _ 2, (hQy.pow 2).div_mul_cancel_left,
hQy.inv_mul_cancel_right]
