equation_negAdd — Mathlib

English

The condition that a point lies on the sum of two given points is equivalent to the addPolynomial evaluated at the x-coordinate of the sum being zero.

Русский

Условие, что точка принадлежит сумме двух данных точек, эквивалентно тому, что addPolynomial по абсциссе суммы даёт ноль.

LaTeX

$$$ W'.Equation (W'.addX x_1 x_2 \ell) (W'.negAddY x_1 x_2 y_1 \ell) \iff (W'.addPolynomial x_1 y_1 \ell).eval (W'.addX x_1 x_2 \ell) = 0 $$$

Lean4

theorem equation_negAdd {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.negAddY x₁ x₂ y₁ <| W.slope x₁ x₂ y₁ y₂) :=
  by
  rw [equation_add_iff, addPolynomial_slope h₁ h₂ hxy]
  eval_simp
  rw [neg_eq_zero, sub_self, mul_zero]

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