slope_fun_def_field — Mathlib

English

For field-valued functions, slope f a equals (f a) shift: slope f a = (f(b) − f(a)) / (b − a) with b variable.

Русский

Для функции, принимающей значения в поле, наклон между a и b равен (f(b) − f(a)) / (b − a).

LaTeX

$$$\operatorname{slope}(f,a) = \lambda b. \dfrac{f(b) - f(a)}{b - a}$$$

Lean4

theorem slope_fun_def_field (f : k → k) (a : k) : slope f a = fun b => (f b - f a) / (b - a) :=
  (div_eq_inv_mul _ _).symm

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