slope_of_Y_ne_eq_evalEval — Mathlib

English

Equivalent presentation of slope in terms of evalEval polynomials when x1 ≠ x2 or x1 = x2 with tangent case.

Русский

Эквивалентное представление наклона через evalEval-полиномы в случае секущей или касательной.

LaTeX

$$$W.slope x_1 x_2 y_1 y_2 = -\frac{P_X(x_1,y_1)}{P_Y(x_1,y_1)}$ при определённых условиях$$

Lean4

theorem slope_of_Y_ne_eq_evalEval {x₁ x₂ y₁ y₂ : F} (hx : x₁ = x₂) (hy : y₁ ≠ W.negY x₂ y₂) :
    W.slope x₁ x₂ y₁ y₂ = -W.polynomialX.evalEval x₁ y₁ / W.polynomialY.evalEval x₁ y₁ :=
  by
  rw [slope_of_Y_ne hx hy, evalEval_polynomialX, neg_sub]
  congr 1
  rw [negY, evalEval_polynomialY]
  ring1

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