slope_def_field

Mathlib.LinearAlgebra.AffineSpace.Slope

URI: https://scilib.ai/kg/mathlib#slope_def_field

English

When k is a field, the slope between a and b equals (f(b)−f(a)) / (b−a).

Русский

Для поля k наклон между a и b равен (f(b)−f(a)) / (b−a).

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru