feat(Wiedijk100Theorems): roots of a quartic

[hanwenzhu]

• Added quartic_eq_zero_iff which gives the roots of the quartic equation in terms of a root u to a particular cubic equation, and a degenerate case quartic_eq_zero_iff_of_q_eq_zero
• Simplified the cubic proof

---

• depends on: [Merged by Bors] - chore(Wiedijk100Theorems): clean up SolutionToCubic #18299

[github-actions]

PR summary 29e425fab0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ cubic_depressed_eq_zero_iff
+ quartic_depressed_eq_zero_iff
+ quartic_eq_zero_iff
+ quartic_eq_zero_iff_of_q_eq_zero
- cubic_basic_eq_zero_iff
- cubic_monic_eq_zero_iff

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[Ruben-VandeVelde]

Meta-point: it's unfortunate that git doesn't recognize that you're moving the cubic. Would you mind creating a separate PR with just the changes to the cubic?

[hanwenzhu]

@Ruben-VandeVelde It's probably also because I changed the file too much. By adding the quartic proof, the file is changed more than 50% so git can't recognize it. I also tested locally if I commit changes to the cubic, and then move to a new file with added quartic, git still can't recognize the name change. Perhaps I can do a separate PR that only contains a file rename to SolutionOfCubicQuartic.lean and changes to the cubic, and in this PR add the quartic proof?

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - chore(Wiedijk100Theorems): clean up SolutionToCubic #18299
  By Dependent Issues (🤖). Happy coding!