dblU_ne_zero_of_Y_eq — Mathlib

English

A variant of the unit criterion for dblU under coordinate relations.

Русский

Вариант критерий единичности dblU при соотношениях координат.

LaTeX

$$$ \\text{IsUnit}(W.dblU P) $$$

Lean4

theorem dblU_ne_zero_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) : W.dblU P ≠ 0 :=
  div_ne_zero (pow_ne_zero 3 ((nonsingular_iff_of_Y_eq_negY hPz <| Y_eq_negY_of_Y_eq hQz hx hy hy').mp hP).right) <|
    pow_ne_zero 2 hPz

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