diff --git a/Mathlib/NumberTheory/FLT/MasonStothers.lean b/Mathlib/NumberTheory/FLT/MasonStothers.lean index 24ac7c089a207..4ac41c664408a 100644 --- a/Mathlib/NumberTheory/FLT/MasonStothers.lean +++ b/Mathlib/NumberTheory/FLT/MasonStothers.lean @@ -59,37 +59,37 @@ theorem max₃_le {a b c d : Nat} : max₃ a b c ≤ d ↔ a ≤ d ∧ b ≤ d /-- For a given polynomial `a`, `divRadical a` is `a` divided by its radical `radical a`.-/ -def divRadical (a : k[X]) : k[X] := a / (radical a) +def divRadical (a : k[X]) : k[X] := a / radical a -theorem hMul_radical_divRadical (a : k[X]) : (radical a) * (divRadical a) = a := by +theorem mul_radical_divRadical (a : k[X]) : radical a * divRadical a = a := by rw [divRadical] rw [← EuclideanDomain.mul_div_assoc] ·refine mul_div_cancel_left₀ _ (radical_ne_zero a) exact radical_dvd_self a theorem divRadical_ne_zero {a : k[X]} (ha : a ≠ 0) : divRadical a ≠ 0 := by - rw [← hMul_radical_divRadical a] at ha + rw [← mul_radical_divRadical a] at ha exact right_ne_zero_of_mul ha theorem divRadical_isUnit {u : k[X]} (hu : IsUnit u) : IsUnit (divRadical u) := by rwa [divRadical, radical_unit_eq_one hu, EuclideanDomain.div_one] -theorem eq_divRadical {a x : k[X]} (h : (radical a) * x = a) : x = divRadical a := by +theorem eq_divRadical {a x : k[X]} (h : radical a * x = a) : x = divRadical a := by apply EuclideanDomain.eq_div_of_mul_eq_left (radical_ne_zero a) rwa [mul_comm] -theorem divRadical_hMul {a b : k[X]} (hc : IsCoprime a b) : - divRadical (a * b) = (divRadical a) * (divRadical b) := by +theorem divRadical_mul {a b : k[X]} (hc : IsCoprime a b) : + divRadical (a * b) = divRadical a * divRadical b := by by_cases ha : a = 0 · rw [ha, MulZeroClass.zero_mul, divRadical, EuclideanDomain.zero_div, MulZeroClass.zero_mul] by_cases hb : b = 0 · rw [hb, MulZeroClass.mul_zero, divRadical, EuclideanDomain.zero_div, MulZeroClass.mul_zero] symm; apply eq_divRadical rw [radical_mul hc] - rw [mul_mul_mul_comm, hMul_radical_divRadical, hMul_radical_divRadical] + rw [mul_mul_mul_comm, mul_radical_divRadical, mul_radical_divRadical] -theorem divRadical_dvd_self (a : k[X]) : (divRadical a) ∣ a := by +theorem divRadical_dvd_self (a : k[X]) : divRadical a ∣ a := by rw [divRadical] apply EuclideanDomain.div_dvd_of_dvd exact radical_dvd_self a @@ -110,7 +110,7 @@ theorem divRadical_dvd_derivative (a : k[X]) : (divRadical a) ∣ (derivative a) · rw [pow_zero, derivative_one] apply dvd_zero · case succ i => - rw [← mul_dvd_mul_iff_left (radical_ne_zero (p ^ i.succ)), hMul_radical_divRadical, + rw [← mul_dvd_mul_iff_left (radical_ne_zero (p ^ i.succ)), mul_radical_divRadical, radical_pow_of_prime hp i.succ_pos, derivative_pow_succ, ← mul_assoc] apply dvd_mul_of_dvd_left rw [mul_comm, mul_assoc] @@ -122,7 +122,7 @@ theorem divRadical_dvd_derivative (a : k[X]) : (divRadical a) ∣ (derivative a) EuclideanDomain.isCoprime_of_dvd (fun ⟨hx, hy⟩ => not_isUnit_zero (hpxy (zero_dvd_iff.mpr hx) (zero_dvd_iff.mpr hy))) fun p hp _ hpx hpy => hp (hpxy hpx hpy) - rw [divRadical_hMul hc, derivative_mul] + rw [divRadical_mul hc, derivative_mul] exact dvd_add (mul_dvd_mul hx (divRadical_dvd_self y)) (mul_dvd_mul (divRadical_dvd_self x) hy) theorem divRadical_dvd_wronskian_left (a b : k[X]) : (divRadical a) ∣ wronskian a b := by @@ -170,8 +170,8 @@ theorem IsCoprime.wronskian_eq_zero_iff {a b : k[X]} (hc : IsCoprime a b) : protected theorem IsCoprime.divRadical {a b : k[X]} (h : IsCoprime a b) : IsCoprime (divRadical a) (divRadical b) := by - rw [← hMul_radical_divRadical a] at h - rw [← hMul_radical_divRadical b] at h + rw [← mul_radical_divRadical a] at h + rw [← mul_radical_divRadical b] at h exact h.of_mul_left_right.of_mul_right_right private theorem abc_subcall {a b c w : k[X]} {hw : w ≠ 0} (wab : w = wronskian a b) (ha : a ≠ 0) @@ -194,16 +194,12 @@ private theorem abc_subcall {a b c w : k[X]} {hw : w ≠ 0} (wab : w = wronskian rw [← Polynomial.natDegree_mul (divRadical_ne_zero habc) (radical_ne_zero (a * b * c))] _ = (a * b * c).natDegree := by - rw [mul_comm _ (radical _)]; rw [hMul_radical_divRadical (a * b * c)] + rw [mul_comm _ (radical _)]; rw [mul_radical_divRadical (a * b * c)] _ = a.natDegree + b.natDegree + c.natDegree := by rw [Polynomial.natDegree_mul hab hc, Polynomial.natDegree_mul ha hb] rw [t3] at t4 exact Nat.lt_of_add_lt_add_left t4 -private theorem rot3_add {a b c : k[X]} : a + b + c = b + c + a := by ring_nf - -private theorem rot3_mul {a b c : k[X]} : a * b * c = b * c * a := by ring_nf - /-- **Polynomial ABC theorem.** -/ theorem Polynomial.abc {a b c : k[X]} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) (hab : IsCoprime a b) (hbc : IsCoprime b c) (hca : IsCoprime c a) (hsum : a + b + c = 0) : @@ -213,7 +209,7 @@ theorem Polynomial.abc {a b c : k[X]} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ have wbc := wronskian_eq_of_sum_zero hsum set w := wronskian a b with wab have wca : w = wronskian c a := by - rw [rot3_add] at hsum + rw [add_rotate] at hsum have h := wronskian_eq_of_sum_zero hsum rw [← wbc] at h; exact h have abc_dr_dvd_w : divRadical (a * b * c) ∣ w := by @@ -229,21 +225,20 @@ theorem Polynomial.abc {a b c : k[X]} (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ have abdr_dvd_w := cop_ab_dr.mul_dvd adr_dvd_w bdr_dvd_w have abcdr_dvd_w := cop_abc_dr.mul_dvd abdr_dvd_w cdr_dvd_w convert abcdr_dvd_w using 1 - rw [← divRadical_hMul hab] - rw [← divRadical_hMul _] + rw [← divRadical_mul hab] + rw [← divRadical_mul _] exact hca.symm.mul_left hbc by_cases hw : w = 0 · right rw [hw] at wab wbc cases' hab.wronskian_eq_zero_iff.mp wab.symm with ga gb cases' hbc.wronskian_eq_zero_iff.mp wbc.symm with _ gc - refine ⟨ga, gb, gc⟩ + exact ⟨ga, gb, gc⟩ · left rw [max₃_add_distrib_right, max₃_le] - constructor - · rw [rot3_mul] at abc_dr_dvd_w ⊢ + refine ⟨?_, ?_, ?_⟩ + · rw [mul_rotate] at abc_dr_dvd_w ⊢ apply abc_subcall wbc <;> assumption - constructor - · rw [rot3_mul, rot3_mul] at abc_dr_dvd_w ⊢ + · rw [mul_rotate, mul_rotate] at abc_dr_dvd_w ⊢ apply abc_subcall wca <;> assumption · apply abc_subcall wab <;> assumption