deriv_id''

Mathlib.Analysis.Calculus.Deriv.Basic

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

English

Another variant asserting deriv of id equals 1.

Русский

Еще один вариант утверждения, что deriv id = 1.

LaTeX

$$$deriv(\\lambda x: x) = \\lambda _ . 1$$$

Lean4

/-- Variant with `fun x => x` rather than `id` -/
@[simp]
theorem deriv_id'' : (deriv fun x : 𝕜 => x) = fun _ => 1 :=
  deriv_id'

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

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

Разделы

Аффилиация

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