logDeriv

Mathlib.FieldTheory.Differential.Basic

URI: https://scilib.ai/kg/mathlib#Differential.logDeriv

English

The logarithmic derivative of a function a is a' / a, where a' denotes the derivative of a.

Русский

Логарифмический производный функции a равен a'/a.

LaTeX

$$$\\mathrm{logDeriv}(a) = a'/a$$$

Lean4

/-- The logarithmic derivative of a is a′ / a.
-/
def logDeriv : R :=
  a′ / a

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

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

Разделы

Аффилиация

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