multiplicity of derivative

Stream: Is there code for X?

[Eric Rodriguez]

for p : ℝ[X], do we have anything like p.derivative.root_multiplicity t = p.root_multiplicity t - 1? (for t a root, of course)

[Reid Barton]

isn't it also true for t not a root? :upside_down:

[Damiano Testa]

(Most of the times, at least! :wink: )

[Eric Rodriguez]

if t isn't a root but it is a critical point it doesn't hold sadly

[Reid Barton]

oh

[Damiano Testa]

Actually, one inequality always holds, right? p.root_multiplicity t - 1 ≤ p.derivative.root_multiplicity t, I think.

[Damiano Testa]

I'm never sure whether I like it or not when Lean's - seems to have better lemmas than the "correct" $-$!

[Eric Rodriguez]

∀ n : ℕ, -1 ≤ n so we're all clear good ;b (e: idioms...)

[Damiano Testa]

Very clear! What I haven't really accepted is that in Lean, the inequality is sometimes realized as an equality.

[Eric Rodriguez]

Eric Rodriguez said:

for p : ℝ[X], do we have anything like p.derivative.root_multiplicity t = p.root_multiplicity t - 1? (for t a root, of course)

"fun" fact - this doesn't hold even for fields, and I should've known it from flt-regular! X^p - 1 = (X - 1)^p has multiplicity p in zmod p, but its derivative pX^(n-1) = 0 has multiplicity zero

[Eric Rodriguez]

i'm just going to stick a char-zero assumption and be done with it...

[Eric Rodriguez]

#12856