deriv_const' — Mathlib

English

The derivative of the constant function f(t) = c is the zero function; i.e., deriv (fun t => c) is identically 0.

Русский

Производная константной функции f(t) = c есть нулевая функция; то есть deriv(функция константы) тождественно равна 0.

LaTeX

$$$\\operatorname{deriv}(\\lambda t. c) = 0$$$

Lean4

@[simp]
theorem deriv_const' : (deriv fun _ : 𝕜 => c) = fun _ => 0 :=
  funext fun x => deriv_const x c

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