repeated roots

Stream: new members

[Nicholas Wilson]

How would I sate the hypothesis that a function( ℝ → ℝ, or ℂ → ℂ) has no repeated roots?

[Jireh Loreaux]

What's your definition of a repeated root? Are these functions polynomials? Are they analytic? Or even just differentiable?

[Nicholas Wilson]

err... I guess for every x : f x = 0 the tangent line of f at x is order Θ(x)? Not necessarily but most likely polynomials times some other function. Yes. Yes

I guess I should say: is there something in Mathlib that I should be using instead, or should I roll my own?

[Riccardo Brasca]

Before formalizing any statement you should write down a very precise mathematical statement. If you are talking about polynomials it should be very easy, otherwise it depends on what exactly you are talking about.

[Floris van Doorn]

For polynomials, there is docs#Polynomial.roots which gives the roots of a polynomial, including their multiplicities.

[Nicholas Wilson]

Thanks.

[Eric Wieser]

You might want docs#Polynomial.aroots if you have real coefficients but want to consider complex roots