isUnit_dblU_of_Y_eq — Mathlib

English

If P,Q satisfy the Y-equality condition, then dblZ P equals zero exactly when the Y-relations impose a specific relation with Q.

Русский

Если P,Q удовлетворяют условию равенства Y, dblZ P равно нулю тогда и только тогда, когда Y-отношения накладывают конкретное отношение с Q.

LaTeX

$$$\text{If } P,Q \text{ satisfy the Y-equality, then } W'.dblZ P = 0$$$

Lean4

theorem isUnit_dblU_of_Y_eq {P Q : Fin 3 → F} (hP : W.Nonsingular P) (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)
    (hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3) : IsUnit (W.dblU P) :=
  (dblU_ne_zero_of_Y_eq hP hPz hQz hx hy hy').isUnit

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