chore(Wiedijk100Theorems): clean up SolutionToCubic (#18299)

* Shortened the cubic formula proof by removing unnecessary `cubic_monic_eq_zero_iff`
* Renamed `basic` to `depressed`
* Added clearer module docstring
* Renamed the file to SolutionToCubicQuartic, so that #18290 can show correct diffs

Archive.lean

@@ -62,6 +62,6 @@ import Archive.Wiedijk100Theorems.InverseTriangleSum
 import Archive.Wiedijk100Theorems.Konigsberg
 import Archive.Wiedijk100Theorems.Partition
 import Archive.Wiedijk100Theorems.PerfectNumbers
-import Archive.Wiedijk100Theorems.SolutionOfCubic
+import Archive.Wiedijk100Theorems.SolutionOfCubicQuartic
 import Archive.Wiedijk100Theorems.SumOfPrimeReciprocalsDiverges
 import Archive.ZagierTwoSquares

Archive/Wiedijk100Theorems/SolutionOfCubic.lean → Archive/Wiedijk100Theorems/SolutionOfCubicQuartic.lean

@@ -1,32 +1,40 @@
 /-
 Copyright (c) 2022 Jeoff Lee. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jeoff Lee
+Authors: Jeoff Lee, Thomas Zhu
 -/
 import Mathlib.Tactic.LinearCombination
 import Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
 
 /-!
-# The Solution of a Cubic
+# The roots of cubic polynomials
 
 This file proves Theorem 37 from the [100 Theorems List](https://www.cs.ru.nl/~freek/100/).
 
-In this file, we give the solutions to the cubic equation `a * x^3 + b * x^2 + c * x + d = 0`
-over a field `K` that has characteristic neither 2 nor 3, that has a third primitive root of
-unity, and in which certain other quantities admit square and cube roots.
-
-This is based on the [Cardano's Formula](https://en.wikipedia.org/wiki/Cubic_equation#Cardano's_formula).
+We give the solutions to the cubic equation `a * x^3 + b * x^2 + c * x + d = 0` over a field `K`
+that has characteristic neither 2 nor 3, that has a third primitive root of
+unity, and in which certain other quantities admit square and cube roots. This is based on the
+[Cardano's Formula](https://en.wikipedia.org/wiki/Cubic_equation#Cardano's_formula).
 
 ## Main statements
 
-- `cubic_eq_zero_iff` : gives the roots of the cubic equation
+- `cubic_eq_zero_iff`: gives the roots of the cubic equation
 where the discriminant `p = 3 * a * c - b^2` is nonzero.
-- `cubic_eq_zero_iff_of_p_eq_zero` : gives the roots of the cubic equation
+- `cubic_eq_zero_iff_of_p_eq_zero`: gives the roots of the cubic equation
 where the discriminant equals zero.
 
+## Proof outline
+
+1.  Given cubic $ax^3 + bx^2 + cx + d = 0$, we show it is equivalent to some "depressed cubic"
+    $y^3 + 3py - 2q = 0$ where $y = x + b / (3a)$, $p = (3ac - b^2) / (9a^2)$, and
+    $q = (9abc - 2b^3 - 27a^2d) / (54a^3)$ (`h₁` in `cubic_eq_zero_iff`).
+2.  When $p$ is zero, this is easily solved (`cubic_eq_zero_iff_of_p_eq_zero`).
+3.  Otherwise one can directly derive a factorization of the depressed cubic, in terms of some
+    primitive cube root of unity $\omega^3 = 1$ (`cubic_depressed_eq_zero_iff`).
+
 ## References
 
-Originally ported from Isabelle/HOL. The
+The cubic formula was originally ported from Isabelle/HOL. The
 [original file](https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Cubic_Quartic.html) was written by Amine Chaieb.
 
 ## Tags
@@ -41,13 +49,15 @@ section Field
 
 open Polynomial
 
-variable {K : Type*} [Field K] (a b c d : K) {ω p q r s t : K}
+variable {K : Type*} [Field K] (a b c d e : K) {ω p q r s t u v w x y : K}
+
+section Cubic
 
 theorem cube_root_of_unity_sum (hω : IsPrimitiveRoot ω 3) : 1 + ω + ω ^ 2 = 0 := by
   simpa [cyclotomic_prime, Finset.sum_range_succ] using hω.isRoot_cyclotomic (by decide)
 
-/-- The roots of a monic cubic whose quadratic term is zero and whose discriminant is nonzero. -/
-theorem cubic_basic_eq_zero_iff (hω : IsPrimitiveRoot ω 3) (hp_nonzero : p ≠ 0)
+/-- The roots of a monic cubic whose quadratic term is zero and whose linear term is nonzero. -/
+theorem cubic_depressed_eq_zero_iff (hω : IsPrimitiveRoot ω 3) (hp_nonzero : p ≠ 0)
     (hr : r ^ 2 = q ^ 2 + p ^ 3) (hs3 : s ^ 3 = q + r) (ht : t * s = p) (x : K) :
     x ^ 3 + 3 * p * x - 2 * q = 0 ↔ x = s - t ∨ x = s * ω - t * ω ^ 2 ∨ x = s * ω ^ 2 - t * ω := by
   have h₁ : ∀ x a₁ a₂ a₃ : K, x = a₁ ∨ x = a₂ ∨ x = a₃ ↔ (x - a₁) * (x - a₂) * (x - a₃) = 0 := by
@@ -66,23 +76,6 @@ theorem cubic_basic_eq_zero_iff (hω : IsPrimitiveRoot ω 3) (hp_nonzero : p ≠
 
 variable [Invertible (2 : K)] [Invertible (3 : K)]
 
-/-- Roots of a monic cubic whose discriminant is nonzero. -/
-theorem cubic_monic_eq_zero_iff (hω : IsPrimitiveRoot ω 3) (hp : p = (3 * c - b ^ 2) / 9)
-    (hp_nonzero : p ≠ 0) (hq : q = (9 * b * c - 2 * b ^ 3 - 27 * d) / 54)
-    (hr : r ^ 2 = q ^ 2 + p ^ 3) (hs3 : s ^ 3 = q + r) (ht : t * s = p) (x : K) :
-    x ^ 3 + b * x ^ 2 + c * x + d = 0 ↔
-      x = s - t - b / 3 ∨ x = s * ω - t * ω ^ 2 - b / 3 ∨ x = s * ω ^ 2 - t * ω - b / 3 := by
-  let y := x + b / 3
-  have hi2 : (2 : K) ≠ 0 := Invertible.ne_zero _
-  have hi3 : (3 : K) ≠ 0 := Invertible.ne_zero _
-  have h9 : (9 : K) = 3 ^ 2 := by norm_num
-  have h54 : (54 : K) = 2 * 3 ^ 3 := by norm_num
-  have h₁ : x ^ 3 + b * x ^ 2 + c * x + d = y ^ 3 + 3 * p * y - 2 * q := by
-    rw [hp, hq]
-    field_simp [y, h9, h54]; ring
-  rw [h₁, cubic_basic_eq_zero_iff hω hp_nonzero hr hs3 ht y]
-  simp_rw [eq_sub_iff_add_eq]
-
 /-- **The Solution of Cubic**.
   The roots of a cubic polynomial whose discriminant is nonzero. -/
 theorem cubic_eq_zero_iff (ha : a ≠ 0) (hω : IsPrimitiveRoot ω 3)
@@ -92,25 +85,17 @@ theorem cubic_eq_zero_iff (ha : a ≠ 0) (hω : IsPrimitiveRoot ω 3)
     a * x ^ 3 + b * x ^ 2 + c * x + d = 0 ↔
       x = s - t - b / (3 * a) ∨
         x = s * ω - t * ω ^ 2 - b / (3 * a) ∨ x = s * ω ^ 2 - t * ω - b / (3 * a) := by
-  have hi3 : (3 : K) ≠ 0 := Invertible.ne_zero _
+  let y := x + b / (3 * a)
   have h9 : (9 : K) = 3 ^ 2 := by norm_num
   have h54 : (54 : K) = 2 * 3 ^ 3 := by norm_num
-  have h₁ : a * x ^ 3 + b * x ^ 2 + c * x + d
-    = a * (x ^ 3 + b / a * x ^ 2 + c / a * x + d / a) := by field_simp; ring
+  have h₁ : a * x ^ 3 + b * x ^ 2 + c * x + d = a * (y ^ 3 + 3 * p * y - 2 * q) := by
+    rw [hp, hq]
+    simp [field_simps, y, ha, h9, h54]; ring
   have h₂ : ∀ x, a * x = 0 ↔ x = 0 := by intro x; simp [ha]
-  have hp' : p = (3 * (c / a) - (b / a) ^ 2) / 9 := by field_simp [hp, h9]; ring_nf
-  have hq' : q = (9 * (b / a) * (c / a) - 2 * (b / a) ^ 3 - 27 * (d / a)) / 54 := by
-    rw [hq, h54]
-    simp [field_simps, ha]
-    ring_nf
-  rw [h₁, h₂, cubic_monic_eq_zero_iff (b / a) (c / a) (d / a) hω hp' hp_nonzero hq' hr hs3 ht x]
-  have h₄ :=
-    calc
-      b / a / 3 = b / (a * 3) := by field_simp [ha]
-      _ = b / (3 * a) := by rw [mul_comm]
-  rw [h₄]
+  rw [h₁, h₂, cubic_depressed_eq_zero_iff hω hp_nonzero hr hs3 ht]
+  simp_rw [eq_sub_iff_add_eq]
 
-/-- the solution of the cubic equation when p equals zero. -/
+/-- The solution of the cubic equation when p equals zero. -/
 theorem cubic_eq_zero_iff_of_p_eq_zero (ha : a ≠ 0) (hω : IsPrimitiveRoot ω 3)
     (hpz : 3 * a * c - b ^ 2 = 0)
     (hq : q = (9 * a * b * c - 2 * b ^ 3 - 27 * a ^ 2 * d) / (54 * a ^ 3)) (hs3 : s ^ 3 = 2 * q)
@@ -144,6 +129,8 @@ theorem cubic_eq_zero_iff_of_p_eq_zero (ha : a ≠ 0) (hω : IsPrimitiveRoot ω
   rw [h₁, h₂, h₃, h₄ (x + b / (3 * a))]
   ring_nf
 
+end Cubic
+
 end Field
 
 end Theorems100