slope_of_Y_ne — Mathlib

English

If x1 = x2 and y1 ≠ W.negY x2 y2, then slope equals -W.polynomialX.evalEval x1 y1 / W.polynomialY.evalEval x1 y1.

Русский

Если x1 = x2 и y1 ≠ W.negY x2 y2, то наклон равен -W.polynomialX.evalEval x1 y1 делённому на W.polynomialY.evalEval x1 y1.

LaTeX

$$$W.slope x_1 x_2 y_1 y_2 = -\dfrac{W.polynomialX.evalEval x_1 y_1}{W.polynomialY.evalEval x_1 y_1}$$$

Lean4

theorem slope_of_Y_ne {x₁ x₂ y₁ y₂ : F} (hx : x₁ = x₂) (hy : y₁ ≠ W.negY x₂ y₂) :
    W.slope x₁ x₂ y₁ y₂ = (3 * x₁ ^ 2 + 2 * W.a₂ * x₁ + W.a₄ - W.a₁ * y₁) / (y₁ - W.negY x₁ y₁) := by simp_all

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