derivative_ofNat — Mathlib

English

Derivative of the natural cast to polynomials is zero (equivalently, derivative(ofNat(n)) = 0 for n ≥ 2).

Русский

Производная от приведения натурального числа в полиномы равна нулю (то есть derivative(ofNat(n)) = 0 при n ≥ 2).

LaTeX

$$$\operatorname{derivative}(\text{ofNat}(n)) = 0$$$

Lean4

@[simp]
theorem derivative_ofNat (n : ℕ) [n.AtLeastTwo] : derivative (ofNat(n) : R[X]) = 0 :=
  derivative_natCast

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