Quadratic, cubic, and quartic formulas

Stream: new members

[Benjamin]

Does mathlib have theorems for the quadratic, cubic, or quartic formulas? If not, I'm curious if it'd be feasible for a Lean beginner to prove them.

[Johan Commelin]

Nope, we don't. Sounds like a nice first project

[Benjamin]

Is that a no to all three?

[Johan Commelin]

Probably quadratic is around somewhere...

[Kenny Lau]

docs#quadratic_eq_zero_iff

[Kenny Lau]

I got this by searching for quadratic

[Alex J. Best]

Sounds good! Might be best to work in complex or an algebraically closed field for the cubic and quartic versions though.
Actually the quadratic one could have a version for any characteristic not 2 field (not just a linear ordered field).

[Kevin Buzzard]

Yes, I got one of my kids to implement the quadratic formula as part of their work experience and they did it for any field of characteristic not 2, and the statement was that if the discriminant has a square root then...

[Benjamin]

Would it be preferable to implement the solutions in terms of the discriminant like was done for the quadratic case, or to just list the solutions directly in terms of the coefficients?

[Alex J. Best]

I would say assume algebraically closed and express it in terms of the coefficients.

[Mario Carneiro]

The way I expressed the core version of the quadratic/cubic/quartic formulas in metamath is to have a hypothesis saying things like x^3 = ... and y^2 = ..., so that the main proof can be done in any ring with characteristic not 2 or 3.

[Alex J. Best]

I guess having both as part of the API isn't actually much harder anyway, http://us.metamath.org/mpegif/cubic.html

[Mario Carneiro]

I don't think we have a nice way to work with nth roots over algebraically closed fields right now, but you could specialize this theorem to real using real.sqrt and real.rpow

[Mario Carneiro]

the core version I mentioned is http://us.metamath.org/mpegif/cubic2.html

[Mario Carneiro]

it's more general anyway, since it allows you to pick either the positive or negative square root, or any of the three cube roots in an alg closed field

[Mario Carneiro]

You might be amused by http://us.metamath.org/mpegif/quartfull.html, where all substitutions are performed into the quartic formula

[Benjamin]

Mario Carneiro said:

The way I expressed the core version of the quadratic/cubic/quartic formulas in metamath is to have a hypothesis saying things like x^3 = ... and y^2 = ..., so that the main proof can be done in any ring with characteristic not 2 or 3.

What is y here?

[Mario Carneiro]

y is the square root of some subexpression

[Mario Carneiro]

for example, for the quadratic formula instead of writing +- sqrt (b^2 + 4*a*c) you have a hypothesis y^2 = b^2 + 4*a*c and then use y

[Mario Carneiro]

you will end up with a disjunction like x = (-b + y) / 2*a \/ x = (-b - y) / 2*a

[Benjamin]

I see thanks

[Mario Carneiro]

that way you don't need to know that square roots actually exist in the ring you are working over, since you are given whichever roots you need, but to use the theorem you have to provide a root or else it is trivial. I'm not sure exactly under what conditions you can reverse the implication and prove that the root exists given a root of the quadratic

[Benjamin]

I'm not very good at reading metamath proofs (or formal proofs in general yet), but did you basically proceed by plugging in the equations to the polynomial to verify that they're roots? And then how did you prove that they are the only solutions?

[Mario Carneiro]

No, the proof does not jut plug in the solutions, because it's easier to just maintain the biconditional at all times. The proof strategy is to perform things like "subtract on both sides" or "multiply by a nonzero constant" which preserve the biconditional, algebraic expansions (which preserve equality, and could be done by ring), and the key fact x^2 = y^2 <-> x = y \/ x = -y and a similar version for cube roots.

[Mario Carneiro]

You could plug in the solutions but that's a lot of expansion work and it won't make the reverse direction any easier

[Mario Carneiro]

I of course didn't invent the proof; Cardano has the claim I believe. Wikipedia has an overview of it

[Mario Carneiro]

The metamath proof cubic proves $ax^3+bx^2+cx+d=0$ by reducing it to mcubic, which proves $x^3+ax^2+bx+c=0$ by reducing it to dcubic, which proves $x^3+px+q=0\iff \exists r(r^3=1\land x=rt-m/rt)$ (where $m$ and $t$ are formulas in terms of $p,q$), by plugging into the equation in the reverse direction (dcubic1), and for the forward direction (dcubic2) first solving the equation $x=u-m/u$ for $u$, and then using it to derive an equation for $r$.

[Mario Carneiro]

I think this is a version of Vieta's substitution on wiki

[Benjamin]

Thanks, this is helpful. I probably won't get to this for a while (if at all). I'm still learning Lean, but if I get around to trying to contribute to mathlib this is what I'll try.

[Kevin Buzzard]

It's a great thing to work on for a beginner

[Kenny Lau]

Ian Stewart's book on Galois Theory has a proof using Galois Theory