Loogle!

Result

Found 276 declarations mentioning Polynomial.derivative. Of these, only the first 200 are shown.

• Polynomial.derivative 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] : Polynomial R →ₗ[R] Polynomial R
• Polynomial.derivative_X 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] : Polynomial.derivative Polynomial.X = 1
• Polynomial.degree_derivative_le 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {p : Polynomial R} : (Polynomial.derivative p).degree ≤ p.degree
• Polynomial.derivative_natCast 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {n : ℕ} : Polynomial.derivative ↑n = 0
• Polynomial.natDegree_derivative_lt 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.natDegree ≠ 0) : (Polynomial.derivative p).natDegree < p.natDegree
• Polynomial.natDegree_derivative_le 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (p : Polynomial R) : (Polynomial.derivative p).natDegree ≤ p.natDegree - 1
• Polynomial.derivative_one 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] : Polynomial.derivative 1 = 0
• Polynomial.derivative_zero 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] : Polynomial.derivative 0 = 0
• Polynomial.natDegree_iterate_derivative 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (p : Polynomial R) (k : ℕ) : ((⇑Polynomial.derivative)^[k] p).natDegree ≤ p.natDegree - k
• Polynomial.derivative_of_natDegree_zero 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p.natDegree = 0) : Polynomial.derivative p = 0
• Polynomial.derivative_ofNat 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (n : ℕ) [n.AtLeastTwo] : Polynomial.derivative (OfNat.ofNat n) = 0
• Polynomial.iterate_derivative_X 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {k : ℕ} (h : 1 < k) : (⇑Polynomial.derivative)^[k] Polynomial.X = 0
• Polynomial.iterate_derivative_eq_zero 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {p : Polynomial R} {x : ℕ} (hx : p.natDegree < x) : (⇑Polynomial.derivative)^[x] p = 0
• Polynomial.iterate_derivative_zero 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {k : ℕ} : (⇑Polynomial.derivative)^[k] 0 = 0
• Polynomial.natDegree_derivative 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] [IsAddTorsionFree R] (p : Polynomial R) : (Polynomial.derivative p).natDegree = p.natDegree - 1
• Polynomial.degree_derivative_lt 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {p : Polynomial R} (hp : p ≠ 0) : (Polynomial.derivative p).degree < p.degree
• Polynomial.natDegree_eq_zero_of_derivative_eq_zero 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {p : Polynomial R} [IsAddTorsionFree R] : Polynomial.derivative p = 0 → p.natDegree = 0
• Polynomial.derivative_eq_zero 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {p : Polynomial R} [IsAddTorsionFree R] : Polynomial.derivative p = 0 ↔ p.natDegree = 0
• Polynomial.derivative_ne_zero 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {p : Polynomial R} [IsAddTorsionFree R] : Polynomial.derivative p ≠ 0 ↔ p.natDegree ≠ 0
• Polynomial.iterate_derivative_one 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {k : ℕ} (h : 0 < k) : (⇑Polynomial.derivative)^[k] 1 = 0
• Polynomial.of_mem_support_derivative 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {p : Polynomial R} {n : ℕ} (h : n ∈ (Polynomial.derivative p).support) : n + 1 ∈ p.support
• Polynomial.leadingCoeff_derivative 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] [IsAddTorsionFree R] (p : Polynomial R) : (Polynomial.derivative p).leadingCoeff = p.leadingCoeff * ↑p.natDegree
• Polynomial.degree_derivative 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {p : Polynomial R} [IsAddTorsionFree R] (hp : p.natDegree ≠ 0) : (Polynomial.derivative p).degree = ↑(p.natDegree - 1)
• Polynomial.degree_derivative_eq 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] [IsAddTorsionFree R] (p : Polynomial R) (hp : 0 < p.natDegree) : (Polynomial.derivative p).degree = ↑(p.natDegree - 1)
• Polynomial.derivative_C 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {a : R} : Polynomial.derivative (Polynomial.C a) = 0
• Polynomial.mem_support_derivative 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} {n : ℕ} [Semiring R] {p : Polynomial R} [IsAddTorsionFree R] : n ∈ (Polynomial.derivative p).support ↔ n + 1 ∈ p.support
• Polynomial.iterate_derivative_C 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} {a : R} [Semiring R] {k : ℕ} (h : 0 < k) : (⇑Polynomial.derivative)^[k] (Polynomial.C a) = 0
• Polynomial.derivative_X_add_C 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (c : R) : Polynomial.derivative (Polynomial.X + Polynomial.C c) = 1
• Polynomial.derivative_eval 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (p : Polynomial R) (x : R) : Polynomial.eval x (Polynomial.derivative p) = p.sum fun n a => a * ↑n * x ^ (n - 1)
• Polynomial.coeff_iterate_derivative 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {k : ℕ} (p : Polynomial R) (m : ℕ) : ((⇑Polynomial.derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
• Polynomial.derivative_intCast 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Ring R] {n : ℤ} : Polynomial.derivative ↑n = 0
• Polynomial.eq_C_of_derivative_eq_zero 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {p : Polynomial R} [IsAddTorsionFree R] (h : Polynomial.derivative p = 0) : p = Polynomial.C (p.coeff 0)
• Polynomial.derivative_C_mul_X 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (a : R) : Polynomial.derivative (Polynomial.C a * Polynomial.X) = Polynomial.C a
• Polynomial.coeff_derivative 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (p : Polynomial R) (n : ℕ) : (Polynomial.derivative p).coeff n = p.coeff (n + 1) * (↑n + 1)
• Polynomial.derivative_X_sq 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] : Polynomial.derivative (Polynomial.X ^ 2) = Polynomial.C 2 * Polynomial.X
• Polynomial.derivative_map 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (p : Polynomial R) (f : R →+* S) : Polynomial.derivative (Polynomial.map f p) = Polynomial.map f (Polynomial.derivative p)
• Polynomial.derivative_apply 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (p : Polynomial R) : Polynomial.derivative p = p.sum fun n a => Polynomial.C (a * ↑n) * Polynomial.X ^ (n - 1)
• Polynomial.derivative_sum 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} {ι : Type y} [Semiring R] {s : Finset ι} {f : ι → Polynomial R} : Polynomial.derivative (∑ b ∈ s, f b) = ∑ b ∈ s, Polynomial.derivative (f b)
• Polynomial.derivative_X_pow 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (n : ℕ) : Polynomial.derivative (Polynomial.X ^ n) = Polynomial.C ↑n * Polynomial.X ^ (n - 1)
• Polynomial.iterate_derivative_map 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} {S : Type v} [Semiring R] [Semiring S] (p : Polynomial R) (f : R →+* S) (k : ℕ) : (⇑Polynomial.derivative)^[k] (Polynomial.map f p) = Polynomial.map f ((⇑Polynomial.derivative)^[k] p)
• Polynomial.iterate_derivative_sum 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} {ι : Type y} [Semiring R] (k : ℕ) (s : Finset ι) (f : ι → Polynomial R) : (⇑Polynomial.derivative)^[k] (∑ b ∈ s, f b) = ∑ b ∈ s, (⇑Polynomial.derivative)^[k] (f b)
• Polynomial.dvd_derivative_iff 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] [NoZeroDivisors R] {P : Polynomial R} : P ∣ Polynomial.derivative P ↔ Polynomial.derivative P = 0
• Polynomial.derivative_natCast_mul 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {n : ℕ} {f : Polynomial R} : Polynomial.derivative (↑n * f) = ↑n * Polynomial.derivative f
• Polynomial.dvd_iterate_derivative_pow 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] (f : Polynomial R) (n : ℕ) {m : ℕ} (c : R) (hm : m ≠ 0) : ↑n ∣ Polynomial.eval c ((⇑Polynomial.derivative)^[m] (f ^ n))
• Polynomial.derivative_X_pow_succ 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (n : ℕ) : Polynomial.derivative (Polynomial.X ^ (n + 1)) = Polynomial.C (↑n + 1) * Polynomial.X ^ n
• Polynomial.iterate_derivative_natCast_mul 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {n k : ℕ} {f : Polynomial R} : (⇑Polynomial.derivative)^[k] (↑n * f) = ↑n * (⇑Polynomial.derivative)^[k] f
• Polynomial.derivative_X_sub_C 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Ring R] (c : R) : Polynomial.derivative (Polynomial.X - Polynomial.C c) = 1
• Polynomial.derivativeFinsupp_apply_apply 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (p : Polynomial R) (x✝ : ℕ) : (Polynomial.derivativeFinsupp p) x✝ = (⇑Polynomial.derivative)^[x✝] p
• Polynomial.derivative_C_mul_X_sq 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (a : R) : Polynomial.derivative (Polynomial.C a * Polynomial.X ^ 2) = Polynomial.C (a * 2) * Polynomial.X
• Polynomial.derivative_monomial 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (a : R) (n : ℕ) : Polynomial.derivative ((Polynomial.monomial n) a) = (Polynomial.monomial (n - 1)) (a * ↑n)
• Polynomial.derivative_smul 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] [IsScalarTower S R R] (s : S) (p : Polynomial R) : Polynomial.derivative (s • p) = s • Polynomial.derivative p
• Polynomial.iterate_derivative_eq_zero_of_degree_lt 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommRing R] {k : ℕ} {P : Polynomial R} (h : P.degree < ↑k) : (⇑Polynomial.derivative)^[k] P = 0
• Polynomial.pow_sub_dvd_iterate_derivative_pow 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] (p : Polynomial R) (n m : ℕ) : p ^ (n - m) ∣ (⇑Polynomial.derivative)^[m] (p ^ n)
• Polynomial.iterate_derivative_smul 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {S : Type u_1} [SMulZeroClass S R] [IsScalarTower S R R] (s : S) (p : Polynomial R) (k : ℕ) : (⇑Polynomial.derivative)^[k] (s • p) = s • (⇑Polynomial.derivative)^[k] p
• Polynomial.derivative_C_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (a : R) (n : ℕ) : Polynomial.derivative (Polynomial.C a * Polynomial.X ^ n) = Polynomial.C (a * ↑n) * Polynomial.X ^ (n - 1)
• Polynomial.derivative_monomial_succ 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (a : R) (n : ℕ) : Polynomial.derivative ((Polynomial.monomial (n + 1)) a) = (Polynomial.monomial n) (a * (↑n + 1))
• Polynomial.iterate_derivative_X_pow_eq_natCast_mul 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] (n k : ℕ) : (⇑Polynomial.derivative)^[k] (Polynomial.X ^ n) = ↑(n.descFactorial k) * Polynomial.X ^ (n - k)
• Polynomial.derivative_C_mul 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (a : R) (p : Polynomial R) : Polynomial.derivative (Polynomial.C a * p) = Polynomial.C a * Polynomial.derivative p
• Polynomial.iterate_derivative_C_mul 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (a : R) (p : Polynomial R) (k : ℕ) : (⇑Polynomial.derivative)^[k] (Polynomial.C a * p) = Polynomial.C a * (⇑Polynomial.derivative)^[k] p
• Polynomial.derivative_add 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {f g : Polynomial R} : Polynomial.derivative (f + g) = Polynomial.derivative f + Polynomial.derivative g
• Polynomial.pow_sub_one_dvd_derivative_of_pow_dvd 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] {p q : Polynomial R} {n : ℕ} (dvd : q ^ n ∣ p) : q ^ (n - 1) ∣ Polynomial.derivative p
• Polynomial.pow_sub_dvd_iterate_derivative_of_pow_dvd 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] {p q : Polynomial R} {n : ℕ} (m : ℕ) (dvd : q ^ n ∣ p) : q ^ (n - m) ∣ (⇑Polynomial.derivative)^[m] p
• Polynomial.iterate_derivative_X_pow_eq_smul 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] (n k : ℕ) : (⇑Polynomial.derivative)^[k] (Polynomial.X ^ n) = ↑(n.descFactorial k) • Polynomial.X ^ (n - k)
• Polynomial.derivative_neg 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Ring R] (f : Polynomial R) : Polynomial.derivative (-f) = -Polynomial.derivative f
• Polynomial.iterate_derivative_neg 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Ring R] {f : Polynomial R} {k : ℕ} : (⇑Polynomial.derivative)^[k] (-f) = -(⇑Polynomial.derivative)^[k] f
• Polynomial.iterate_derivative_X_pow_eq_C_mul 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] (n k : ℕ) : (⇑Polynomial.derivative)^[k] (Polynomial.X ^ n) = Polynomial.C ↑(n.descFactorial k) * Polynomial.X ^ (n - k)
• Polynomial.iterate_derivative_eq_sum 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (p : Polynomial R) (k : ℕ) : (⇑Polynomial.derivative)^[k] p = ∑ x ∈ ((⇑Polynomial.derivative)^[k] p).support, Polynomial.C ((x + k).descFactorial k • p.coeff (x + k)) * Polynomial.X ^ x
• Polynomial.derivative_mul 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {f g : Polynomial R} : Polynomial.derivative (f * g) = Polynomial.derivative f * g + f * Polynomial.derivative g
• Polynomial.iterate_derivative_eq_factorial_smul_sum 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (p : Polynomial R) (k : ℕ) : (⇑Polynomial.derivative)^[k] p = k.factorial • ∑ x ∈ ((⇑Polynomial.derivative)^[k] p).support, Polynomial.C ((x + k).choose k • p.coeff (x + k)) * Polynomial.X ^ x
• Polynomial.iterate_derivative_mul 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] {n : ℕ} (p q : Polynomial R) : (⇑Polynomial.derivative)^[n] (p * q) = ∑ k ∈ Finset.range n.succ, n.choose k • ((⇑Polynomial.derivative)^[n - k] p * (⇑Polynomial.derivative)^[k] q)
• Polynomial.derivative_intCast_mul 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Ring R] {n : ℤ} {f : Polynomial R} : Polynomial.derivative (↑n * f) = ↑n * Polynomial.derivative f
• Polynomial.eval_multiset_prod_X_sub_C_derivative 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommRing R] [DecidableEq R] {S : Multiset R} {r : R} (hr : r ∈ S) : Polynomial.eval r (Polynomial.derivative (Multiset.map (fun a => Polynomial.X - Polynomial.C a) S).prod) = (Multiset.map (fun a => r - a) (S.erase r)).prod
• Polynomial.iterate_derivative_intCast_mul 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Ring R] {n : ℤ} {k : ℕ} {f : Polynomial R} : (⇑Polynomial.derivative)^[k] (↑n * f) = ↑n * (⇑Polynomial.derivative)^[k] f
• Polynomial.derivative_prod_finset 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} {ι : Type y} [CommSemiring R] [DecidableEq ι] {s : Finset ι} {f : ι → Polynomial R} : Polynomial.derivative (∏ b ∈ s, f b) = ∑ a ∈ s, (∏ b ∈ s.erase a, f b) * Polynomial.derivative (f a)
• Polynomial.iterate_derivative_X_sub_pow_self 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommRing R] (n : ℕ) (c : R) : (⇑Polynomial.derivative)^[n] ((Polynomial.X - Polynomial.C c) ^ n) = ↑n.factorial
• Polynomial.derivative_prod 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} {ι : Type y} [CommSemiring R] [DecidableEq ι] {s : Multiset ι} {f : ι → Polynomial R} : Polynomial.derivative (Multiset.map f s).prod = (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * Polynomial.derivative (f i)) s).sum
• Polynomial.derivative_pow_eq_zero 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] [NoZeroDivisors R] {n : ℕ} (chn : ↑n ≠ 0) {a : Polynomial R} : Polynomial.derivative (a ^ n) = 0 ↔ Polynomial.derivative a = 0
• Polynomial.iterate_derivative_X_add_pow 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] (n k : ℕ) (c : R) : (⇑Polynomial.derivative)^[k] ((Polynomial.X + Polynomial.C c) ^ n) = n.descFactorial k • (Polynomial.X + Polynomial.C c) ^ (n - k)
• Polynomial.derivative_X_add_C_sq 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] (c : R) : Polynomial.derivative ((Polynomial.X + Polynomial.C c) ^ 2) = Polynomial.C 2 * (Polynomial.X + Polynomial.C c)
• Polynomial.derivative_sq 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] (p : Polynomial R) : Polynomial.derivative (p ^ 2) = Polynomial.C 2 * p * Polynomial.derivative p
• Polynomial.derivative_X_add_C_pow 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] (c : R) (m : ℕ) : Polynomial.derivative ((Polynomial.X + Polynomial.C c) ^ m) = Polynomial.C ↑m * (Polynomial.X + Polynomial.C c) ^ (m - 1)
• Polynomial.derivative_comp 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] (p q : Polynomial R) : Polynomial.derivative (p.comp q) = Polynomial.derivative q * (Polynomial.derivative p).comp q
• Polynomial.derivative_pow 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] (p : Polynomial R) (n : ℕ) : Polynomial.derivative (p ^ n) = Polynomial.C ↑n * p ^ (n - 1) * Polynomial.derivative p
• Polynomial.derivative_sub 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Ring R] {f g : Polynomial R} : Polynomial.derivative (f - g) = Polynomial.derivative f - Polynomial.derivative g
• Polynomial.iterate_derivative_mul_X_pow 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] (n m : ℕ) (p : Polynomial R) : (⇑Polynomial.derivative)^[n] (p * Polynomial.X ^ m) = ∑ k ∈ Finset.range (min m n).succ, (n.choose k * m.descFactorial k) • ((⇑Polynomial.derivative)^[n - k] p * Polynomial.X ^ (m - k))
• Polynomial.derivative_eval₂_C 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] (p q : Polynomial R) : Polynomial.derivative (Polynomial.eval₂ Polynomial.C q p) = Polynomial.eval₂ Polynomial.C q (Polynomial.derivative p) * Polynomial.derivative q
• Polynomial.iterate_derivative_sub 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Ring R] {k : ℕ} {f g : Polynomial R} : (⇑Polynomial.derivative)^[k] (f - g) = (⇑Polynomial.derivative)^[k] f - (⇑Polynomial.derivative)^[k] g
• Polynomial.derivative_pow_succ 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] (p : Polynomial R) (n : ℕ) : Polynomial.derivative (p ^ (n + 1)) = Polynomial.C (↑n + 1) * p ^ n * Polynomial.derivative p
• Polynomial.derivativeFinsupp_derivative 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [Semiring R] (p : Polynomial R) : Polynomial.derivativeFinsupp (Polynomial.derivative p) = Finsupp.comapDomain Nat.succ (Polynomial.derivativeFinsupp p) ⋯
• Polynomial.iterate_derivative_prod_X_sub_C 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommRing R] {k : ℕ} {S : Finset R} (hk : k ≤ S.card) : (⇑Polynomial.derivative)^[k] (∏ a ∈ S, (Polynomial.X - Polynomial.C a)) = ↑k.factorial * ∑ T ∈ Finset.powersetCard (S.card - k) S, ∏ a ∈ T, (Polynomial.X - Polynomial.C a)
• Polynomial.derivative_comp_one_sub_X 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommRing R] (p : Polynomial R) : Polynomial.derivative (p.comp (1 - Polynomial.X)) = -(Polynomial.derivative p).comp (1 - Polynomial.X)
• Polynomial.iterate_derivative_X_sub_pow 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommRing R] (n k : ℕ) (c : R) : (⇑Polynomial.derivative)^[k] ((Polynomial.X - Polynomial.C c) ^ n) = n.descFactorial k • (Polynomial.X - Polynomial.C c) ^ (n - k)
• Polynomial.iterate_derivative_mul_X 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] {n : ℕ} (p : Polynomial R) : (⇑Polynomial.derivative)^[n] (p * Polynomial.X) = (⇑Polynomial.derivative)^[n] p * Polynomial.X + n • (⇑Polynomial.derivative)^[n - 1] p
• Polynomial.derivative_X_sub_C_sq 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommRing R] (c : R) : Polynomial.derivative ((Polynomial.X - Polynomial.C c) ^ 2) = Polynomial.C 2 * (Polynomial.X - Polynomial.C c)
• Polynomial.derivative_X_sub_C_pow 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommRing R] (c : R) (m : ℕ) : Polynomial.derivative ((Polynomial.X - Polynomial.C c) ^ m) = Polynomial.C ↑m * (Polynomial.X - Polynomial.C c) ^ (m - 1)
• Polynomial.iterate_derivative_comp_one_sub_X 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommRing R] (p : Polynomial R) (k : ℕ) : (⇑Polynomial.derivative)^[k] (p.comp (1 - Polynomial.X)) = (-1) ^ k * ((⇑Polynomial.derivative)^[k] p).comp (1 - Polynomial.X)
• Polynomial.iterate_derivative_derivative_mul_X 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] {n : ℕ} (p : Polynomial R) : (⇑Polynomial.derivative)^[n] (Polynomial.derivative p * Polynomial.X) = (⇑Polynomial.derivative)^[n + 1] p * Polynomial.X + n • (⇑Polynomial.derivative)^[n] p
• Polynomial.iterate_derivative_derivative_mul_X_sq 📋 Mathlib.Algebra.Polynomial.Derivative
  {R : Type u} [CommSemiring R] {n : ℕ} (p : Polynomial R) : (⇑Polynomial.derivative)^[n] ((⇑Polynomial.derivative)^[2] p * Polynomial.X ^ 2) = (⇑Polynomial.derivative)^[n + 2] p * Polynomial.X ^ 2 + (2 * n) • (⇑Polynomial.derivative)^[n + 1] p * Polynomial.X + (n * (n - 1)) • (⇑Polynomial.derivative)^[n] p
• Polynomial.expand_contract' 📋 Mathlib.Algebra.Polynomial.Expand
  {R : Type u} [CommSemiring R] (p : ℕ) [ExpChar R p] [NoZeroDivisors R] {f : Polynomial R} (hf : Polynomial.derivative f = 0) : (Polynomial.expand R p) (Polynomial.contract p f) = f
• Polynomial.expand_contract 📋 Mathlib.Algebra.Polynomial.Expand
  {R : Type u} [CommSemiring R] (p : ℕ) [CharP R p] [NoZeroDivisors R] {f : Polynomial R} (hf : Polynomial.derivative f = 0) (hp : p ≠ 0) : (Polynomial.expand R p) (Polynomial.contract p f) = f
• Polynomial.derivative_expand 📋 Mathlib.Algebra.Polynomial.Expand
  {R : Type u} [CommSemiring R] (p : ℕ) (f : Polynomial R) : Polynomial.derivative ((Polynomial.expand R p) f) = (Polynomial.expand R p) (Polynomial.derivative f) * (↑p * Polynomial.X ^ (p - 1))
• Polynomial.isRoot_iterate_derivative_of_lt_rootMultiplicity 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ} (hn : n < Polynomial.rootMultiplicity t p) : ((⇑Polynomial.derivative)^[n] p).IsRoot t
• Polynomial.rootMultiplicity_sub_one_le_derivative_rootMultiplicity 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] [NoZeroDivisors R] [CharZero R] (p : Polynomial R) (t : R) : Polynomial.rootMultiplicity t p - 1 ≤ Polynomial.rootMultiplicity t (Polynomial.derivative p)
• Polynomial.derivative_rootMultiplicity_of_root 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] [NoZeroDivisors R] [CharZero R] {p : Polynomial R} {t : R} (hpt : p.IsRoot t) : Polynomial.rootMultiplicity t (Polynomial.derivative p) = Polynomial.rootMultiplicity t p - 1
• Polynomial.one_lt_rootMultiplicity_iff_isRoot 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} (h : p ≠ 0) : 1 < Polynomial.rootMultiplicity t p ↔ p.IsRoot t ∧ (Polynomial.derivative p).IsRoot t
• Polynomial.one_lt_rootMultiplicity_iff_isRoot_iterate_derivative 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} (h : p ≠ 0) : 1 < Polynomial.rootMultiplicity t p ↔ ∀ m ≤ 1, ((⇑Polynomial.derivative)^[m] p).IsRoot t
• Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] [NoZeroDivisors R] [CharZero R] {p : Polynomial R} {t : R} {n : ℕ} (h : p ≠ 0) (hroot : ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t) : n < Polynomial.rootMultiplicity t p
• Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] [NoZeroDivisors R] [CharZero R] {p : Polynomial R} {t : R} {n : ℕ} (h : p ≠ 0) : n < Polynomial.rootMultiplicity t p ↔ ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t
• Polynomial.one_lt_rootMultiplicity_iff_isRoot_gcd 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] [GCDMonoid (Polynomial R)] {p : Polynomial R} {t : R} (h : p ≠ 0) : 1 < Polynomial.rootMultiplicity t p ↔ (gcd p (Polynomial.derivative p)).IsRoot t
• Polynomial.derivative_rootMultiplicity_of_root_of_mem_nonZeroDivisors 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} (hpt : p.IsRoot t) (hnzd : ↑(Polynomial.rootMultiplicity t p) ∈ nonZeroDivisors R) : Polynomial.rootMultiplicity t (Polynomial.derivative p) = Polynomial.rootMultiplicity t p - 1
• Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ} (h : p ≠ 0) (hroot : ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t) (hnzd : ↑n.factorial ∈ nonZeroDivisors R) : n < Polynomial.rootMultiplicity t p
• Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ} (h : p ≠ 0) (hnzd : ↑n.factorial ∈ nonZeroDivisors R) : n < Polynomial.rootMultiplicity t p ↔ ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t
• Polynomial.lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors' 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ} (h : p ≠ 0) (hroot : ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t) (hnzd : ∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R) : n < Polynomial.rootMultiplicity t p
• Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors' 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} {n : ℕ} (h : p ≠ 0) (hnzd : ∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R) : n < Polynomial.rootMultiplicity t p ↔ ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t
• Polynomial.isRoot_of_isRoot_of_dvd_derivative_mul 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] [NoZeroDivisors R] [CharZero R] {f g : Polynomial R} (hf0 : f ≠ 0) (hfd : f ∣ Polynomial.derivative f * g) {a : R} (haf : f.IsRoot a) : g.IsRoot a
• Polynomial.eval_iterate_derivative_rootMultiplicity 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] {p : Polynomial R} {t : R} : Polynomial.eval t ((⇑Polynomial.derivative)^[Polynomial.rootMultiplicity t p] p) = (Polynomial.rootMultiplicity t p).factorial • Polynomial.eval t (p /ₘ (Polynomial.X - Polynomial.C t) ^ Polynomial.rootMultiplicity t p)
• Polynomial.rootMultiplicity_sub_one_le_derivative_rootMultiplicity_of_ne_zero 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {R : Type u} [CommRing R] (p : Polynomial R) (t : R) (hnezero : Polynomial.derivative p ≠ 0) : Polynomial.rootMultiplicity t p - 1 ≤ Polynomial.rootMultiplicity t (Polynomial.derivative p)
• Polynomial.isCoprime_of_is_root_of_eval_derivative_ne_zero 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {K : Type u_1} [Field K] (f : Polynomial K) (a : K) (hf' : Polynomial.eval a (Polynomial.derivative f) ≠ 0) : IsCoprime (Polynomial.X - Polynomial.C a) (f /ₘ (Polynomial.X - Polynomial.C a))
• Polynomial.X_sub_C_dvd_derivative_of_X_sub_C_dvd_divByMonic 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {K : Type u_1} [Field K] (f : Polynomial K) {a : K} (hf : Polynomial.X - Polynomial.C a ∣ f /ₘ (Polynomial.X - Polynomial.C a)) : Polynomial.X - Polynomial.C a ∣ Polynomial.derivative f
• Polynomial.divByMonic_add_X_sub_C_mul_derivative_divByMonic_eq_derivative 📋 Mathlib.Algebra.Polynomial.FieldDivision
  {K : Type u_1} [CommRing K] (f : Polynomial K) (a : K) : f /ₘ (Polynomial.X - Polynomial.C a) + (Polynomial.X - Polynomial.C a) * Polynomial.derivative (f /ₘ (Polynomial.X - Polynomial.C a)) = Polynomial.derivative f
• Polynomial.binomExpansion 📋 Mathlib.Algebra.Polynomial.Identities
  {R : Type u} [CommRing R] (f : Polynomial R) (x y : R) : { k // Polynomial.eval (x + y) f = Polynomial.eval x f + Polynomial.eval x (Polynomial.derivative f) * y + k * y ^ 2 }
• Matrix.derivative_det_one_add_X_smul 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
  {R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) : Polynomial.eval 0 (Polynomial.derivative (1 + Polynomial.X • M.map ⇑Polynomial.C).det) = M.trace
• Matrix.derivative_det_one_add_X_smul_aux 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
  {R : Type u} [CommRing R] {n : ℕ} (M : Matrix (Fin n) (Fin n) R) : Polynomial.eval 0 (Polynomial.derivative (1 + Polynomial.X • M.map ⇑Polynomial.C).det) = M.trace
• Polynomial.hasseDeriv_one 📋 Mathlib.Algebra.Polynomial.HasseDeriv
  {R : Type u_1} [Semiring R] : Polynomial.hasseDeriv 1 = Polynomial.derivative
• Polynomial.hasseDeriv_one' 📋 Mathlib.Algebra.Polynomial.HasseDeriv
  {R : Type u_1} [Semiring R] (f : Polynomial R) : (Polynomial.hasseDeriv 1) f = Polynomial.derivative f
• Polynomial.factorial_smul_hasseDeriv 📋 Mathlib.Algebra.Polynomial.HasseDeriv
  {R : Type u_1} [Semiring R] (k : ℕ) : ⇑(k.factorial • Polynomial.hasseDeriv k) = (⇑Polynomial.derivative)^[k]
• Polynomial.taylor_coeff_one 📋 Mathlib.Algebra.Polynomial.Taylor
  {R : Type u_1} [Semiring R] (r : R) (f : Polynomial R) : ((Polynomial.taylor r) f).coeff 1 = Polynomial.eval r (Polynomial.derivative f)
• Polynomial.eval_add_of_sq_eq_zero 📋 Mathlib.Algebra.Polynomial.Taylor
  {R : Type u_1} [CommSemiring R] (p : Polynomial R) (x y : R) (hy : y ^ 2 = 0) : Polynomial.eval (x + y) p = Polynomial.eval x p + Polynomial.eval x (Polynomial.derivative p) * y
• Polynomial.exists_mul_sq_add_linear_part_eq_eval_add 📋 Mathlib.Algebra.Polynomial.Taylor
  {R : Type u_1} [CommSemiring R] (p : Polynomial R) (x y : R) : ∃ c, c * y ^ 2 + Polynomial.eval x (Polynomial.derivative p) * y + Polynomial.eval x p = Polynomial.eval (x + y) p
• Polynomial.aeval_add_of_sq_eq_zero 📋 Mathlib.Algebra.Polynomial.Taylor
  {R : Type u_1} [CommSemiring R] {S : Type u_2} [CommRing S] [Algebra R S] (p : Polynomial R) (x y : S) (hy : y ^ 2 = 0) : (Polynomial.aeval (x + y)) p = (Polynomial.aeval x) p + (Polynomial.aeval x) (Polynomial.derivative p) * y
• Polynomial.Splits.eval_root_derivative 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] [DecidableEq R] (hf : f.Splits) (hm : f.Monic) {x : R} (hx : x ∈ f.roots) : Polynomial.eval x (Polynomial.derivative f) = (Multiset.map (fun x_1 => x - x_1) (f.roots.erase x)).prod
• Polynomial.Splits.eval_derivative 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [CommRing R] {f : Polynomial R} [IsDomain R] [DecidableEq R] (hf : f.Splits) (x : R) : Polynomial.eval x (Polynomial.derivative f) = f.leadingCoeff * (Multiset.map (fun a => (Multiset.map (fun x_1 => x - x_1) (f.roots.erase a)).prod) f.roots).sum
• Polynomial.Splits.eval_derivative_div_eval_of_ne_zero 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f : Polynomial R} (hf : f.Splits) {x : R} (hx : Polynomial.eval x f ≠ 0) : Polynomial.eval x (Polynomial.derivative f) / Polynomial.eval x f = (Multiset.map (fun z => 1 / (x - z)) f.roots).sum
• Polynomial.Splits.eval_derivative_eq_eval_mul_sum 📋 Mathlib.Algebra.Polynomial.Splits
  {R : Type u_1} [Field R] {f : Polynomial R} (hf : f.Splits) {x : R} (hx : Polynomial.eval x f ≠ 0) : Polynomial.eval x (Polynomial.derivative f) = Polynomial.eval x f * (Multiset.map (fun z => 1 / (x - z)) f.roots).sum
• Derivation.map_aeval 📋 Mathlib.RingTheory.Derivation.Basic
  {R : Type u_1} {A : Type u_2} {M : Type u_4} [CommSemiring R] [CommSemiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] (D : Derivation R A M) (P : Polynomial R) (x : A) : D ((Polynomial.aeval x) P) = (Polynomial.aeval x) (Polynomial.derivative P) • D x
• Polynomial.separable_def 📋 Mathlib.FieldTheory.Separable
  {R : Type u} [CommSemiring R] (f : Polynomial R) : f.Separable ↔ IsCoprime f (Polynomial.derivative f)
• Polynomial.Separable.eval₂_derivative_ne_zero 📋 Mathlib.FieldTheory.Separable
  {R : Type u} [CommSemiring R] {S : Type v} [CommSemiring S] [Nontrivial S] (f : R →+* S) {p : Polynomial R} (h : p.Separable) {x : S} (hx : Polynomial.eval₂ f x p = 0) : Polynomial.eval₂ f x (Polynomial.derivative p) ≠ 0
• Polynomial.separable_def' 📋 Mathlib.FieldTheory.Separable
  {R : Type u} [CommSemiring R] (f : Polynomial R) : f.Separable ↔ ∃ a b, a * f + b * Polynomial.derivative f = 1
• Polynomial.Separable.aeval_derivative_ne_zero 📋 Mathlib.FieldTheory.Separable
  {R : Type u} [CommSemiring R] {S : Type v} [CommSemiring S] [Nontrivial S] [Algebra R S] {p : Polynomial R} (h : p.Separable) {x : S} (hx : (Polynomial.aeval x) p = 0) : (Polynomial.aeval x) (Polynomial.derivative p) ≠ 0
• Polynomial.separable_iff_derivative_ne_zero 📋 Mathlib.FieldTheory.Separable
  {F : Type u} [Field F] {f : Polynomial F} (hf : Irreducible f) : f.Separable ↔ Polynomial.derivative f ≠ 0
• Polynomial.newtonMap_apply_of_not_isUnit 📋 Mathlib.Dynamics.Newton
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P : Polynomial R} {x : S} (h : ¬IsUnit ((Polynomial.aeval x) (Polynomial.derivative P))) : P.newtonMap x = x
• Polynomial.isFixedPt_newtonMap_of_isUnit_iff 📋 Mathlib.Dynamics.Newton
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P : Polynomial R} {x : S} (h : IsUnit ((Polynomial.aeval x) (Polynomial.derivative P))) : Function.IsFixedPt P.newtonMap x ↔ (Polynomial.aeval x) P = 0
• Polynomial.newtonMap_apply 📋 Mathlib.Dynamics.Newton
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (P : Polynomial R) {x : S} : P.newtonMap x = x - Ring.inverse ((Polynomial.aeval x) (Polynomial.derivative P)) * (Polynomial.aeval x) P
• Polynomial.existsUnique_nilpotent_sub_and_aeval_eq_zero 📋 Mathlib.Dynamics.Newton
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P : Polynomial R} {x : S} (h : IsNilpotent ((Polynomial.aeval x) P)) (h' : IsUnit ((Polynomial.aeval x) (Polynomial.derivative P))) : ∃! r, IsNilpotent (x - r) ∧ (Polynomial.aeval r) P = 0
• Polynomial.aeval_pow_two_pow_dvd_aeval_iterate_newtonMap 📋 Mathlib.Dynamics.Newton
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P : Polynomial R} {x : S} (h : IsNilpotent ((Polynomial.aeval x) P)) (h' : IsUnit ((Polynomial.aeval x) (Polynomial.derivative P))) (n : ℕ) : (Polynomial.aeval x) P ^ 2 ^ n ∣ (Polynomial.aeval (P.newtonMap^[n] x)) P
• Polynomial.newtonMap_apply_of_isUnit 📋 Mathlib.Dynamics.Newton
  {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {P : Polynomial R} {x : S} (h : IsUnit ((Polynomial.aeval x) (Polynomial.derivative P))) : P.newtonMap x = x - ↑h.unit⁻¹ * (Polynomial.aeval x) P
• Polynomial.isRoot_of_isRoot_iff_dvd_derivative_mul 📋 Mathlib.FieldTheory.IsAlgClosed.Basic
  {K : Type u_1} [Field K] [IsAlgClosed K] [CharZero K] {f g : Polynomial K} (hf0 : f ≠ 0) : (∀ (x : K), f.IsRoot x → g.IsRoot x) ↔ f ∣ Polynomial.derivative f * g
• Lagrange.eval_nodal_derivative_eval_node_eq 📋 Mathlib.LinearAlgebra.Lagrange
  {R : Type u_1} [CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} [DecidableEq ι] {i : ι} (hi : i ∈ s) : Polynomial.eval (v i) (Polynomial.derivative (Lagrange.nodal s v)) = Polynomial.eval (v i) (Lagrange.nodal (s.erase i) v)
• Lagrange.derivative_nodal 📋 Mathlib.LinearAlgebra.Lagrange
  {R : Type u_1} [CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} [DecidableEq ι] : Polynomial.derivative (Lagrange.nodal s v) = ∑ i ∈ s, Lagrange.nodal (s.erase i) v
• Lagrange.nodalWeight_eq_eval_derivative_nodal 📋 Mathlib.LinearAlgebra.Lagrange
  {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} {i : ι} (hi : i ∈ s) : Lagrange.nodalWeight s v i = (Polynomial.eval (v i) (Polynomial.derivative (Lagrange.nodal s v)))⁻¹
• Lagrange.eval_iterate_derivative_eq_sum 📋 Mathlib.LinearAlgebra.Lagrange
  {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} (hvs : Set.InjOn v ↑s) {P : Polynomial F} (hP : P.degree < ↑s.card) {k : ℕ} (hk : k < s.card) (x : F) : Polynomial.eval x ((⇑Polynomial.derivative)^[k] P) = ↑k.factorial * ∑ i ∈ s, (Polynomial.eval (v i) P / ∏ j ∈ s.erase i, (v i - v j)) * ∑ t ∈ Finset.powersetCard (s.card - (k + 1)) (s.erase i), ∏ a ∈ t, (x - v a)
• Lagrange.iterate_derivative_interpolate 📋 Mathlib.LinearAlgebra.Lagrange
  {F : Type u_1} [Field F] {ι : Type u_2} [DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F) (hvs : Set.InjOn v ↑s) {k : ℕ} (hk : k < s.card) : (⇑Polynomial.derivative)^[k] ((Lagrange.interpolate s v) r) = ↑k.factorial * ∑ i ∈ s, Polynomial.C (r i / ∏ j ∈ s.erase i, (v i - v j)) * ∑ t ∈ Finset.powersetCard (s.card - (k + 1)) (s.erase i), ∏ a ∈ t, (Polynomial.X - Polynomial.C (v a))
• Polynomial.Chebyshev.derivative_T_eval_one 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {R : Type u_1} [CommRing R] (n : ℤ) : Polynomial.eval 1 (Polynomial.derivative (Polynomial.Chebyshev.T R n)) = ↑n ^ 2
• Polynomial.Chebyshev.T_derivative_eq_U 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {R : Type u_1} [CommRing R] (n : ℤ) : Polynomial.derivative (Polynomial.Chebyshev.T R n) = ↑n * Polynomial.Chebyshev.U R (n - 1)
• Polynomial.Chebyshev.iterate_derivative_T_eval_one 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {R : Type u_1} [CommRing R] (n : ℤ) (k : ℕ) : ↑(∏ l ∈ Finset.range k, (2 * l + 1)) * Polynomial.eval 1 ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T R n)) = ↑(∏ l ∈ Finset.range k, (n ^ 2 - ↑l ^ 2))
• Polynomial.Chebyshev.derivative_U_eval_one 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {R : Type u_1} [CommRing R] (n : ℤ) : 3 * Polynomial.eval 1 (Polynomial.derivative (Polynomial.Chebyshev.U R n)) = (↑n + 2) * (↑n + 1) * ↑n
• Polynomial.Chebyshev.iterate_derivative_U_eval_one 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {R : Type u_1} [CommRing R] (n : ℤ) (k : ℕ) : ↑(∏ l ∈ Finset.range k, (2 * l + 3)) * Polynomial.eval 1 ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.U R n)) = ↑(∏ l ∈ Finset.range k, ((n + 1) ^ 2 - (↑l + 1) ^ 2)) * (↑n + 1)
• Polynomial.Chebyshev.T_derivative_mem_span_T 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {R : Type u_1} [CommRing R] (n : ℕ) : Polynomial.derivative (Polynomial.Chebyshev.T R ↑n) ∈ Submodule.span ℕ ((fun m => Polynomial.Chebyshev.T R ↑m) '' Set.Ico 0 n)
• Polynomial.Chebyshev.iterate_derivative_T_eval_one_eq_div 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {𝔽 : Type u_3} [Field 𝔽] [CharZero 𝔽] (n : ℤ) (k : ℕ) : Polynomial.eval 1 ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T 𝔽 n)) = ↑(∏ l ∈ Finset.range k, (n ^ 2 - ↑l ^ 2)) / ↑(∏ l ∈ Finset.range k, (2 * l + 1))
• Polynomial.Chebyshev.T_iterate_derivative_mem_span_T 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {R : Type u_1} [CommRing R] (n k : ℕ) : (⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T R ↑n) ∈ Submodule.span ℕ ((fun m => Polynomial.Chebyshev.T R ↑m) '' Set.Icc 0 (n - k))
• Polynomial.Chebyshev.iterate_derivative_U_eval_one_eq_div 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {𝔽 : Type u_3} [Field 𝔽] [CharZero 𝔽] (n : ℤ) (k : ℕ) : Polynomial.eval 1 ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.U 𝔽 n)) = ↑(∏ l ∈ Finset.range k, ((n + 1) ^ 2 - (↑l + 1) ^ 2)) * (↑n + 1) / ↑(∏ l ∈ Finset.range k, (2 * l + 3))
• Polynomial.Chebyshev.derivative_U_eval_one_eq_div 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {𝔽 : Type u_3} [Field 𝔽] [neZero3 : NeZero 3] (n : ℤ) : Polynomial.eval 1 (Polynomial.derivative (Polynomial.Chebyshev.U 𝔽 n)) = (↑n + 2) * (↑n + 1) * ↑n / 3
• Polynomial.Chebyshev.add_one_mul_T_eq_poly_in_U 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {R : Type u_1} [CommRing R] (n : ℤ) : (↑n + 1) * Polynomial.Chebyshev.T R (n + 1) = Polynomial.X * Polynomial.Chebyshev.U R n - (1 - Polynomial.X ^ 2) * Polynomial.derivative (Polynomial.Chebyshev.U R n)
• Polynomial.Chebyshev.one_sub_X_sq_mul_derivative_T_eq_poly_in_T 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {R : Type u_1} [CommRing R] (n : ℤ) : (1 - Polynomial.X ^ 2) * Polynomial.derivative (Polynomial.Chebyshev.T R (n + 1)) = (↑n + 1) * (Polynomial.Chebyshev.T R n - Polynomial.X * Polynomial.Chebyshev.T R (n + 1))
• Polynomial.Chebyshev.iterate_derivative_T_eval_zero_recurrence 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {R : Type u_1} [CommRing R] (n : ℤ) (k : ℕ) : Polynomial.eval 0 ((⇑Polynomial.derivative)^[k + 2] (Polynomial.Chebyshev.T R n)) = -(↑n ^ 2 - ↑k ^ 2) * Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T R n))
• Polynomial.Chebyshev.iterate_derivative_U_eval_zero_recurrence 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {R : Type u_1} [CommRing R] (n : ℤ) (k : ℕ) : Polynomial.eval 0 ((⇑Polynomial.derivative)^[k + 2] (Polynomial.Chebyshev.U R n)) = -((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.U R n))
• Polynomial.Chebyshev.iterate_derivative_T_eval_one_recurrence 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {R : Type u_1} [CommRing R] (n : ℤ) (k : ℕ) : (2 * ↑k + 1) * Polynomial.eval 1 ((⇑Polynomial.derivative)^[k + 1] (Polynomial.Chebyshev.T R n)) = (↑n ^ 2 - ↑k ^ 2) * Polynomial.eval 1 ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T R n))
• Polynomial.Chebyshev.iterate_derivative_U_eval_one_recurrence 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {R : Type u_1} [CommRing R] (n : ℤ) (k : ℕ) : (2 * ↑k + 3) * Polynomial.eval 1 ((⇑Polynomial.derivative)^[k + 1] (Polynomial.Chebyshev.U R n)) = ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * Polynomial.eval 1 ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.U R n))
• Polynomial.Chebyshev.one_sub_X_sq_mul_derivative_derivative_T_eq_poly_in_T 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {R : Type u_1} [CommRing R] (n : ℤ) : (1 - Polynomial.X ^ 2) * (⇑Polynomial.derivative)^[2] (Polynomial.Chebyshev.T R n) = Polynomial.X * Polynomial.derivative (Polynomial.Chebyshev.T R n) - ↑n ^ 2 * Polynomial.Chebyshev.T R n
• Polynomial.Chebyshev.add_one_mul_self_mul_T_eq_poly_in_T 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {R : Type u_1} [CommRing R] (n : ℤ) : (↑n + 1) * ↑n * Polynomial.Chebyshev.T R (n + 1) = ↑n * Polynomial.X * Polynomial.derivative (Polynomial.Chebyshev.T R (n + 1)) - (↑n + 1) * Polynomial.derivative (Polynomial.Chebyshev.T R n)
• Polynomial.Chebyshev.one_sub_X_sq_mul_derivative_derivative_U_eq_poly_in_U 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {R : Type u_1} [CommRing R] (n : ℤ) : (1 - Polynomial.X ^ 2) * (⇑Polynomial.derivative)^[2] (Polynomial.Chebyshev.U R n) = 3 * Polynomial.X * Polynomial.derivative (Polynomial.Chebyshev.U R n) - (↑n + 2) * ↑n * Polynomial.Chebyshev.U R n
• Polynomial.Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_eval 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {R : Type u_1} [CommRing R] (n : ℤ) (k : ℕ) (x : R) : (1 - x ^ 2) * Polynomial.eval x ((⇑Polynomial.derivative)^[k + 2] (Polynomial.Chebyshev.T R n)) = (2 * ↑k + 1) * x * Polynomial.eval x ((⇑Polynomial.derivative)^[k + 1] (Polynomial.Chebyshev.T R n)) - (↑n ^ 2 - ↑k ^ 2) * Polynomial.eval x ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T R n))
• Polynomial.Chebyshev.one_sub_X_sq_mul_iterate_derivative_U_eval 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {R : Type u_1} [CommRing R] (n : ℤ) (k : ℕ) (x : R) : (1 - x ^ 2) * Polynomial.eval x ((⇑Polynomial.derivative)^[k + 2] (Polynomial.Chebyshev.U R n)) = (2 * ↑k + 3) * x * Polynomial.eval x ((⇑Polynomial.derivative)^[k + 1] (Polynomial.Chebyshev.U R n)) - ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * Polynomial.eval x ((⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.U R n))
• Polynomial.Chebyshev.one_sub_X_sq_mul_iterate_derivative_T_eq_poly_in_T 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {R : Type u_1} [CommRing R] (n : ℤ) (k : ℕ) : (1 - Polynomial.X ^ 2) * (⇑Polynomial.derivative)^[k + 2] (Polynomial.Chebyshev.T R n) = (2 * ↑k + 1) * Polynomial.X * (⇑Polynomial.derivative)^[k + 1] (Polynomial.Chebyshev.T R n) - (↑n ^ 2 - ↑k ^ 2) * (⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.T R n)
• Polynomial.Chebyshev.one_sub_X_sq_mul_iterate_derivative_U_eq_poly_in_U 📋 Mathlib.RingTheory.Polynomial.Chebyshev
  {R : Type u_1} [CommRing R] (n : ℤ) (k : ℕ) : (1 - Polynomial.X ^ 2) * (⇑Polynomial.derivative)^[k + 2] (Polynomial.Chebyshev.U R n) = (2 * ↑k + 3) * Polynomial.X * (⇑Polynomial.derivative)^[k + 1] (Polynomial.Chebyshev.U R n) - ((↑n + 1) ^ 2 - (↑k + 1) ^ 2) * (⇑Polynomial.derivative)^[k] (Polynomial.Chebyshev.U R n)
• Polynomial.derivative'_apply 📋 Mathlib.Algebra.Polynomial.Derivation
  {R : Type u_1} [CommSemiring R] (a : Polynomial R) : Polynomial.derivative' a = Polynomial.derivative a
• Derivation.comp_aeval_eq 📋 Mathlib.Algebra.Polynomial.Derivation
  {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (a : A) (d : Derivation R A M) (f : Polynomial R) : d ((Polynomial.aeval a) f) = (Polynomial.aeval a) (Polynomial.derivative f) • d a
• Polynomial.mkDerivation_apply 📋 Mathlib.Algebra.Polynomial.Derivation
  (R : Type u_1) {A : Type u_2} [CommSemiring R] [AddCommMonoid A] [Module R A] [Module (Polynomial R) A] [IsScalarTower R (Polynomial R) A] (a : A) (f : Polynomial R) : ((Polynomial.mkDerivation R) a) f = Polynomial.derivative f • a
• Derivation.compAEval_eq 📋 Mathlib.Algebra.Polynomial.Derivation
  {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module A M] [Module R M] [IsScalarTower R A M] (a : A) (d : Derivation R A M) (f : Polynomial R) : (d.compAEval a) f = Polynomial.derivative f • (Module.AEval.of R M a) (d a)
• Polynomial.mkDerivation_one_eq_derivative 📋 Mathlib.Algebra.Polynomial.Derivation
  (R : Type u_1) [CommSemiring R] (f : Polynomial R) : ((Polynomial.mkDerivation R) 1) f = Polynomial.derivative f
• KaehlerDifferential.polynomialEquiv_D 📋 Mathlib.RingTheory.Kaehler.Polynomial
  (R : Type u) [CommRing R] (P : Polynomial R) : (KaehlerDifferential.polynomialEquiv R) ((KaehlerDifferential.D R (Polynomial R)) P) = Polynomial.derivative P
• KaehlerDifferential.polynomial_D_apply 📋 Mathlib.RingTheory.Kaehler.Polynomial
  (R : Type u) [CommRing R] (P : Polynomial R) : (KaehlerDifferential.D R (Polynomial R)) P = Polynomial.derivative P • (KaehlerDifferential.D R (Polynomial R)) Polynomial.X
• Derivation.apply_eval_eq 📋 Mathlib.RingTheory.Derivation.MapCoeffs
  {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module A M] [Module R M] (d : Derivation R A M) (x : A) (p : Polynomial A) : d (Polynomial.eval x p) = (PolynomialModule.eval x) (d.mapCoeffs p) + Polynomial.eval x (Polynomial.derivative p) • d x
• Differential.deriv_aeval_eq 📋 Mathlib.RingTheory.Derivation.MapCoeffs
  {A : Type u_1} [CommRing A] [Differential A] {R : Type u_2} [CommRing R] [Differential R] [Algebra A R] [DifferentialAlgebra A R] (x : R) (p : Polynomial A) : ((Polynomial.aeval x) p)′ = (Polynomial.aeval x) (Differential.mapCoeffs p) + (Polynomial.aeval x) (Polynomial.derivative p) * x′
• Derivation.apply_aeval_eq 📋 Mathlib.RingTheory.Derivation.MapCoeffs
  {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {B : Type u_4} {M' : Type u_5} [CommRing B] [Algebra R B] [Algebra A B] [AddCommGroup M'] [Module B M'] [Module R M'] [Module A M'] [IsScalarTower R A B] [IsScalarTower A B M'] (d : Derivation R B M') (x : B) (p : Polynomial A) : d ((Polynomial.aeval x) p) = (PolynomialModule.eval x) ((PolynomialModule.map B LinearMap.id) ((Derivation.compAlgebraMap A d).mapCoeffs p)) + (Polynomial.aeval x) (Polynomial.derivative p) • d x
• Derivation.apply_aeval_eq' 📋 Mathlib.RingTheory.Derivation.MapCoeffs
  {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module A M] [Module R M] (d : Derivation R A M) {B : Type u_4} {M' : Type u_5} [CommRing B] [Algebra R B] [Algebra A B] [AddCommGroup M'] [Module B M'] [Module R M'] [Module A M'] (d' : Derivation R B M') (f : M →ₗ[A] M') (h : ∀ (a : A), f (d a) = d' ((algebraMap A B) a)) (x : B) (p : Polynomial A) : d' ((Polynomial.aeval x) p) = (PolynomialModule.eval x) ((PolynomialModule.map B f) (d.mapCoeffs p)) + (Polynomial.aeval x) (Polynomial.derivative p) • d' x
• Polynomial.Bivariate.pderiv_one_equivMvPolynomial 📋 Mathlib.Algebra.Polynomial.Bivariate
  {R : Type u_1} [CommSemiring R] (p : Polynomial (Polynomial R)) : (MvPolynomial.pderiv 1) ((Polynomial.Bivariate.equivMvPolynomial R) p) = (Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.derivative p)
• Polynomial.exists_iterate_derivative_eq_factorial_smul 📋 Mathlib.Algebra.Polynomial.SumIteratedDerivative
  {R : Type u_1} [Semiring R] (p : Polynomial R) (k : ℕ) : ∃ gp, gp.natDegree ≤ p.natDegree - k ∧ (⇑Polynomial.derivative)^[k] p = k.factorial • gp
• Polynomial.sumIDeriv_apply_of_lt 📋 Mathlib.Algebra.Polynomial.SumIteratedDerivative
  {R : Type u_1} [Semiring R] {p : Polynomial R} {n : ℕ} (hn : p.natDegree < n) : Polynomial.sumIDeriv p = ∑ i ∈ Finset.range n, (⇑Polynomial.derivative)^[i] p
• Polynomial.sumIDeriv_apply 📋 Mathlib.Algebra.Polynomial.SumIteratedDerivative
  {R : Type u_1} [Semiring R] (p : Polynomial R) : Polynomial.sumIDeriv p = ∑ i ∈ Finset.range (p.natDegree + 1), (⇑Polynomial.derivative)^[i] p
• Polynomial.sumIDeriv_apply_of_le 📋 Mathlib.Algebra.Polynomial.SumIteratedDerivative
  {R : Type u_1} [Semiring R] {p : Polynomial R} {n : ℕ} (hn : p.natDegree ≤ n) : Polynomial.sumIDeriv p = ∑ i ∈ Finset.range (n + 1), (⇑Polynomial.derivative)^[i] p
• Polynomial.sumIDeriv_eq_self_add 📋 Mathlib.Algebra.Polynomial.SumIteratedDerivative
  {R : Type u_1} [Semiring R] (p : Polynomial R) : Polynomial.sumIDeriv p = p + Polynomial.derivative (Polynomial.sumIDeriv p)
• Polynomial.sumIDeriv_derivative 📋 Mathlib.Algebra.Polynomial.SumIteratedDerivative
  {R : Type u_1} [Semiring R] (p : Polynomial R) : Polynomial.sumIDeriv (Polynomial.derivative p) = Polynomial.derivative (Polynomial.sumIDeriv p)
• Polynomial.aeval_iterate_derivative_of_ge 📋 Mathlib.Algebra.Polynomial.SumIteratedDerivative
  {R : Type u_1} [CommSemiring R] (A : Type u_3) [CommRing A] [Algebra R A] (p : Polynomial R) (q : ℕ) {k : ℕ} (hk : q ≤ k) : ∃ gp, gp.natDegree ≤ p.natDegree - k ∧ ∀ (r : A), (Polynomial.aeval r) ((⇑Polynomial.derivative)^[k] p) = q.factorial • (Polynomial.aeval r) gp
• Polynomial.aeval_iterate_derivative_of_lt 📋 Mathlib.Algebra.Polynomial.SumIteratedDerivative
  {R : Type u_1} [CommSemiring R] {A : Type u_3} [CommRing A] [Algebra R A] (p : Polynomial R) (q : ℕ) (r : A) {p' : Polynomial A} (hp : Polynomial.map (algebraMap R A) p = (Polynomial.X - Polynomial.C r) ^ q * p') {k : ℕ} (hk : k < q) : (Polynomial.aeval r) ((⇑Polynomial.derivative)^[k] p) = 0
• Polynomial.aeval_iterate_derivative_self 📋 Mathlib.Algebra.Polynomial.SumIteratedDerivative
  {R : Type u_1} [CommSemiring R] {A : Type u_3} [CommRing A] [Algebra R A] (p : Polynomial R) (q : ℕ) (r : A) {p' : Polynomial A} (hp : Polynomial.map (algebraMap R A) p = (Polynomial.X - Polynomial.C r) ^ q * p') : (Polynomial.aeval r) ((⇑Polynomial.derivative)^[q] p) = q.factorial • Polynomial.eval r p'
• WeierstrassCurve.Affine.nonsingular_negAdd_of_eval_derivative_ne_zero 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
  {R : Type r} [CommRing R] {W' : WeierstrassCurve.Affine R} {x₁ x₂ y₁ ℓ : R} (hx' : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)) (hx : Polynomial.eval (W'.addX x₁ x₂ ℓ) (Polynomial.derivative (W'.addPolynomial x₁ y₁ ℓ)) ≠ 0) : W'.Nonsingular (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ)
• WeierstrassCurve.Affine.derivative_addPolynomial_slope 📋 Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
  {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} [DecidableEq F] {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) : Polynomial.derivative (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) = -((Polynomial.X - Polynomial.C x₁) * (Polynomial.X - Polynomial.C x₂) + (Polynomial.X - Polynomial.C x₁) * (Polynomial.X - Polynomial.C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) + (Polynomial.X - Polynomial.C x₂) * (Polynomial.X - Polynomial.C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))
• eval_minpolyDiv_self 📋 Mathlib.FieldTheory.Minpoly.MinpolyDiv
  {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} : Polynomial.eval x (minpolyDiv R x) = (Polynomial.aeval x) (Polynomial.derivative (minpoly R x))
• eval_minpolyDiv_of_aeval_eq_zero 📋 Mathlib.FieldTheory.Minpoly.MinpolyDiv
  {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} [IsDomain S] [DecidableEq S] {y : S} (hy : (Polynomial.aeval y) (minpoly R x) = 0) : Polynomial.eval y (minpolyDiv R x) = if x = y then (Polynomial.aeval x) (Polynomial.derivative (minpoly R x)) else 0

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c