derivative_pow_eq_zero — Mathlib

English

In a commutative ring with no zero divisors, for n ≠ 0, derivative(a^n) = 0 iff derivative(a) = 0.

Русский

В коммутативном кольце без нулевых делителей при n ≠ 0 производная от a^n равна 0 тогда и только тогда, когда производная от a равна 0.

LaTeX

$$$\text{If } (n : R) \neq 0, \quad \operatorname{derivative}(a^n) = 0 \iff \operatorname{derivative}(a) = 0$$$

Lean4

theorem derivative_pow_eq_zero {n : ℕ} (chn : (n : R) ≠ 0) {a : R[X]} : derivative (a ^ n) = 0 ↔ derivative a = 0 :=
  by
  nontriviality R
  rw [← C_ne_zero, C_eq_natCast] at chn
  simp +contextual [derivative_pow, chn]

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