dvd_derivative_iff — Mathlib

English

For any integer n and polynomial f, derivative of (n : R[X]) * f equals n * derivative f.

Русский

Для любого целого n и многочлена f производная от (n)·f равна n·derivative f.

LaTeX

$$$\operatorname{derivative}((n : R[X]) \cdot f) = n \cdot \operatorname{derivative}(f)$$$

Lean4

@[simp]
theorem dvd_derivative_iff {P : R[X]} : P ∣ derivative P ↔ derivative P = 0
    where
  mp
    h := by
    by_cases hP : P = 0
    · simp only [hP, derivative_zero]
    exact eq_zero_of_dvd_of_degree_lt h (degree_derivative_lt hP)
  mpr h := by simp [h]

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