Y_sub_Y_mul_Y_sub_negY — Mathlib

English

A simplified form of Y_sub_Y_mul_Y_sub_negY under standard simplifications.

Русский

Упрощённая форма Y_sub_Y_mul_Y_sub_negY при стандартных упрощениях.

LaTeX

$$$$ \\text{Y_sub_Y_mul_Y_sub_negY}(P,Q) = 0 $$$$

Lean4

theorem Y_sub_Y_mul_Y_sub_negY {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q)
    (hx : P x * Q z ^ 2 = Q x * P z ^ 2) :
    (P y * Q z ^ 3 - Q y * P z ^ 3) * (P y * Q z ^ 3 - W'.negY Q * P z ^ 3) = 0 := by
  linear_combination (norm := (rw [negY]; ring1))
    Q z ^ 6 * (equation_iff P).mp hP - P z ^ 6 * (equation_iff Q).mp hQ +
      (P x ^ 2 * Q z ^ 4 + P x * Q x * P z ^ 2 * Q z ^ 2 + Q x ^ 2 * P z ^ 4 - W'.a₁ * P y * P z * Q z ^ 4 +
              W'.a₂ * P x * P z ^ 2 * Q z ^ 4 +
            W'.a₂ * Q x * P z ^ 4 * Q z ^ 2 +
          W'.a₄ * P z ^ 4 * Q z ^ 4) *
        hx

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