addX_eq' — Mathlib

English

There is a precise equality relating addX to addZ and Z-powers under the prime relation hx.

Русский

Существует точное равенство между addX, addZ и степенями Z в условиях hx.

LaTeX

$$addX' relation: W'.addX P Q * (P z * Q z)^2 = (P y Q z^3 - Q y P z^3)^2 + ...$$

Lean4

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

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