Taylor expansion and double roots

TheoremFirst-order Taylor expansion of a polynomial#✓fully proved

Let \(R\) be a commutative ring, let \(f \in R[X]\) and \(a \in R\), and let \(f'\) be the formal derivative of \(f\). There is a unique polynomial \(g \in R[X]\) such that

\[f = f(a) + f'(a)\,(X - a) + g\,(X - a)^2.\]

theorem existsUnique_taylor_remainder (f : R[X]) (a : R) :
    ∃! g : R[X],
      f = C (f.eval a) + C (f.derivative.eval a) * (X - C a) +
        g * (X - C a) ^ 2

Used by 1

Used byDouble root criterion

TheoremDouble root criterion#✓fully proved

Let \(R\) be a commutative ring, let \(f \in R[x]\) and \(a \in R\), and let \(f'\) be the formal derivative of \(f\). Then \(f(a) = 0\) and \(f'(a) = 0\) if and only if \(f = (x - a)^2 g\) for some \(g \in R[x]\).

public theorem eval_and_derivative_eval_eq_zero_iff (f : R[X]) (a : R) :
    f.eval a = 0 ∧ f.derivative.eval a = 0 ↔
      ∃ g : R[X], f = (X - C a) ^ 2 * g

Sources

ATLAS NumberTheoryI, Corollary 9.13.

Uses 1 · Used by 1

Proof usesFirst-order Taylor expansion of a polynomial

Used byDouble root criterion in divisibility form

TheoremDouble root criterion in divisibility form#✓fully proved

Let \(R\) be a commutative ring, let \(f \in R[x]\) and \(a \in R\), and let \(f'\) be the formal derivative of \(f\). Then \((x - a)^2\) divides \(f\) in \(R[x]\) if and only if \(f(a) = 0\) and \(f'(a) = 0\).

public theorem sq_dvd_iff_eval_and_derivative_eval_eq_zero (f : R[X])
    (a : R) :
    (X - C a) ^ 2 ∣ f ↔ f.eval a = 0 ∧ f.derivative.eval a = 0

Sources

ATLAS NumberTheoryI, Corollary 9.13.

Uses 1 · Used by 1

Proof usesDouble root criterion

Used byA nonvanishing derivative excludes a double root

TheoremA nonvanishing derivative excludes a double root#✓fully proved

Let \(R\) be a commutative ring, let \(f \in R[x]\) and \(a \in R\), and let \(f'\) be the formal derivative of \(f\). If \(f'(a) \neq 0\), then \((x - a)^2\) does not divide \(f\) in \(R[x]\).

No assumption on \(f(a)\) is needed.

public theorem not_sq_dvd_of_derivative_eval_ne_zero
    (f : R[X]) (a : R) (hf' : f.derivative.eval a ≠ 0) :
    ¬ (X - C a) ^ 2 ∣ f

Sources

ATLAS NumberTheoryI, consequence of Corollary 9.13.

Uses 1

Proof usesDouble root criterion in divisibility form

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.