slope_of_Y_ne' — Mathlib

English

Explicit slope formula with x1 = x2 and y1 ≠ W.negY x2 y2: slope equals (3 x1^2 + 2 a2 x1 + a4 - a1 y1) / (y1 - W.negY x1 y1).

Русский

Явная формула наклона при x1 = x2 и y1 ≠ W.negY x2 y2: slope = (3 x1^2 + 2 a2 x1 + a4 - a1 y1) / (y1 - W.negY x1 y1).

LaTeX

$$$W.slope x_1 x_2 y_1 y_2 = \dfrac{3 x_1^2 + 2 a_2 x_1 + a_4 - a_1 y_1}{y_1 - W.negY x_1 y_1}$ given $x_1 = x_2$ and $y_1 ≠ W.negY x_2 y_2$$$

Lean4

@[simp]
theorem slope_of_Y_ne' {x₂ y₁ y₂ : F} (hy : ¬y₁ = -y₂ - W.a₁ * x₂ - W.a₃) :
    W.slope x₂ x₂ y₁ y₂ = (3 * x₂ ^ 2 + 2 * W.a₂ * x₂ + W.a₄ - W.a₁ * y₁) / (y₁ - (-y₁ - W.a₁ * x₂ - W.a₃)) := by
  simp [slope, hy]

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