isUnit_dblU_of_Y_eq — Mathlib

English

Under the prime variant, if the cross-conditions hold, then P_y Q_z = W'.negY Q P_z.

Русский

При вариации prime, если выполняются перекрёстные условия, то P_y Q_z = W'.negY Q P_z.

LaTeX

$$$ P_y Q_z = W'.negY Q P_z $$$

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 = Q x * P z) (hy : P y * Q z = Q y * P z) (hy' : P y * Q z = W.negY Q * P z) : IsUnit (W.dblU P) :=
  (dblU_ne_zero_of_Y_eq hP hPz hQz hx hy hy').isUnit

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