equation_add — Mathlib

English

The derivative of the slope-based addition polynomial is a sum of three quadratic factors in X with shifts at x1, x2, and x3.

Русский

Производная кубического полинома сложения по наклону равна сумме трёх квадратичных множителей в X со сдвигами на x1, x2 и x3.

LaTeX

$$$ \frac{d}{dX} \bigl(W'.addPolynomial x_1 y_1 (W.slope x_1 x_2 y_1 y_2)\bigr) = -((X - C x_1)(X - C x_2) + (X - C x_1)(X - C (W.addX x_1 x_2 (W.slope x_1 x_2 y_1 y_2))) + (X - C x_2)(X - C (W.addX x_1 x_2 (W.slope x_1 x_2 y_1 y_2)))) $$$

Lean4

theorem equation_add {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂)
    (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) :
    W.Equation (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂) (W.addY x₁ x₂ y₁ <| W.slope x₁ x₂ y₁ y₂) :=
  (equation_neg ..).mpr <| equation_negAdd h₁ h₂ hxy

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