logDeriv_id'

Mathlib.Analysis.Calculus.LogDeriv

URI: https://scilib.ai/kg/mathlib#logDeriv_id'

English

logDeriv of a constant function is zero.

Русский

logDeriv константы равно нулю.

LaTeX

$$$\operatorname{logDeriv}_{\mathbb{K}}(\text{const}) = 0$$$

Lean4

@[simp]
theorem logDeriv_id' (x : 𝕜) : logDeriv (·) x = 1 / x :=
  logDeriv_id x

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

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

Разделы

Аффилиация

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