slope_of_Y_eq — 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}$ при условии $x_1=x_2$ и $y_1 \neq W.negY x_2 y_2$$$

Lean4

@[simp]
theorem slope_of_Y_eq {x₁ x₂ y₁ y₂ : F} (hx : x₁ = x₂) (hy : y₁ = W.negY x₂ y₂) : W.slope x₁ x₂ y₁ y₂ = 0 := by
  rw [slope, if_pos hx, if_pos hy]

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