Y_eq_of_Y_ne — Mathlib

English

Under certain relations, equality of Y-terms follows from a non-vanishing condition.

Русский

При некоторых отношениях равенство Y-коэффициентов следует из условия неравенства нулю.

LaTeX

$$$$ \\text{Y}_{eq}(P,Q) $$$$

Lean4

theorem Y_eq_of_Y_ne [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q)
    (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 ≠ Q y * P z ^ 3) : P y * Q z ^ 3 = W'.negY Q * P z ^ 3 :=
  sub_eq_zero.mp <| (mul_eq_zero.mp <| Y_sub_Y_mul_Y_sub_negY hP hQ hx).resolve_left <| sub_ne_zero.mpr hy

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