From 91a4f5866a28f8ac940301faa726e42f4a2f8976 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Fri, 17 Nov 2023 17:33:15 +0100 Subject: [PATCH] Remove some whitespace --- FltRegular/CaseI/AuxLemmas.lean | 4 ++-- FltRegular/FltThree/OddPrimeOrFour.lean | 4 ++-- FltRegular/FltThree/Primes.lean | 9 ++++----- FltRegular/FltThree/Spts.lean | 16 ++++++++-------- 4 files changed, 16 insertions(+), 17 deletions(-) diff --git a/FltRegular/CaseI/AuxLemmas.lean b/FltRegular/CaseI/AuxLemmas.lean index 0314acdd..55135641 100644 --- a/FltRegular/CaseI/AuxLemmas.lean +++ b/FltRegular/CaseI/AuxLemmas.lean @@ -17,8 +17,8 @@ local notation "P" => (⟨p, hpri.pos⟩ : ℕ+) local notation "K" => CyclotomicField P ℚ local notation "R" => 𝓞 K - - + + namespace CaseI theorem two_lt (hp5 : 5 ≤ p) : 2 < p := by linarith diff --git a/FltRegular/FltThree/OddPrimeOrFour.lean b/FltRegular/FltThree/OddPrimeOrFour.lean index fdaefd5e..53798edf 100644 --- a/FltRegular/FltThree/OddPrimeOrFour.lean +++ b/FltRegular/FltThree/OddPrimeOrFour.lean @@ -66,7 +66,7 @@ theorem OddPrimeOrFour.exists_and_dvd {n : ℤ} (n2 : 2 < n) : ∃ p, p ∣ n calc 2 ^ k = 2 ^ 2 * 2 ^ (k - 2) := (pow_mul_pow_sub _ ?_).symm _ = 4 * 2 ^ (k - 2) := by norm_num - + rcases k with (_ | _ | _) · exfalso norm_num at n2 @@ -319,4 +319,4 @@ theorem factorsOddPrimeOrFour.pow (z : ℤ) (n : ℕ) (hz : Even (evenFactorExp factorsOddPrimeOrFour (z ^ n) = n • factorsOddPrimeOrFour z := by simp only [factorsOddPrimeOrFour, nsmul_add, Multiset.nsmul_replicate, evenFactorExp.pow, Nat.mul_div_assoc _ (even_iff_two_dvd.mp hz), oddFactors.pow] -#align factors_odd_prime_or_four.pow factorsOddPrimeOrFour.pow \ No newline at end of file +#align factors_odd_prime_or_four.pow factorsOddPrimeOrFour.pow diff --git a/FltRegular/FltThree/Primes.lean b/FltRegular/FltThree/Primes.lean index ef42abe8..11732bb3 100644 --- a/FltRegular/FltThree/Primes.lean +++ b/FltRegular/FltThree/Primes.lean @@ -29,7 +29,7 @@ theorem Int.factor_div (a x : ℤ) (hodd : Odd x) : set c := a % x with hc by_cases H : 2 * c.natAbs < x.natAbs · exact ⟨a / x, c, Int.emod_add_ediv' a x, H⟩ - · push_neg at H + · push_neg at H refine' ⟨(a + abs x) / x, c - abs x, _, _⟩ · have := self_dvd_abs x rw [Int.add_ediv_of_dvd_right this, add_mul, Int.ediv_mul_cancel this, sub_add_add_cancel, hc, @@ -40,7 +40,7 @@ theorem Int.factor_div (a x : ℤ) (hodd : Odd x) : rw [Int.ofNat_mul, ofNat_two] at H ⊢ have hcnonneg := Int.emod_nonneg a h0' have := Int.emod_lt a h0' - rw [Int.natAbs_of_nonneg hcnonneg] at H + rw [Int.natAbs_of_nonneg hcnonneg] at H rw [← Int.natAbs_neg, neg_sub, Int.natAbs_of_nonneg (sub_nonneg_of_le this.le), mul_sub, sub_lt_iff_lt_add, two_mul, Int.abs_eq_natAbs, add_lt_add_iff_left] apply lt_of_le_of_ne H @@ -57,7 +57,7 @@ nonrec theorem Int.two_not_cube (r : ℤ) : r ^ 3 ≠ 2 :=by apply two_not_cube r.natAbs rw [← Int.natAbs_pow, H] norm_num; decide -#align int.two_not_cube Int.two_not_cube +#align int.two_not_cube Int.two_not_cube -- todo square neg_square and neg_pow_bit0 section @@ -77,5 +77,4 @@ end theorem Int.dvd_mul_cancel_prime' {p k m n : ℤ} (hdvd1 : ¬p ∣ m) (hdvd2 : k ∣ m) (hp : Prime p) (h : k ∣ p * n) : k ∣ n := Irreducible.dvd_of_dvd_mul_left hdvd1 hdvd2 hp.irreducible h -#align int.dvd_mul_cancel_prime' Int.dvd_mul_cancel_prime' - +#align int.dvd_mul_cancel_prime' Int.dvd_mul_cancel_prime' diff --git a/FltRegular/FltThree/Spts.lean b/FltRegular/FltThree/Spts.lean index 2a395e15..4c31bc43 100644 --- a/FltRegular/FltThree/Spts.lean +++ b/FltRegular/FltThree/Spts.lean @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. import Mathlib.Data.Int.Order.Units import Mathlib.NumberTheory.Zsqrtd.Basic import Mathlib.RingTheory.Prime -import FltRegular.FltThree.Primes +import FltRegular.FltThree.Primes theorem Zsqrtd.exists {d : ℤ} (a : ℤ√d) (him : a.im ≠ 0) : ∃ c : ℤ√d, a.norm = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0 := @@ -55,7 +55,7 @@ theorem Spts.mul_of_dvd' {a p : ℤ√(-3)} (hdvd : p.norm ∣ a.norm) (hpprime ring · rw [Zsqrtd.norm_def] ring - obtain ⟨A, HA⟩ : ∃ A : Units ℤ, p.norm ∣ p.re * a.im + A * a.re * p.im := + obtain ⟨A, HA⟩ : ∃ A : Units ℤ, p.norm ∣ p.re * a.im + A * a.re * p.im := by cases' h0 with h0 h0 <;> [(use -1); (use 1)] <;> convert h0 using 1 <;> simp only [Units.val_neg, Units.val_one, neg_mul, one_mul] @@ -65,7 +65,7 @@ theorem Spts.mul_of_dvd' {a p : ℤ√(-3)} (hdvd : p.norm ∣ a.norm) (hpprime (A : ℤ) ^ 2 = ((A ^ 2 : Units ℤ) : ℤ) := (Units.val_pow_eq_pow_val _ _).symm _ = ((1 : Units ℤ) : ℤ) := (congr_arg _ (Int.units_sq A)) _ = 1 := Units.val_one - + · set X : ℤ√(-3) := ⟨p.re * a.re - A * 3 * p.im * a.im, p.re * a.im + A * a.re * p.im⟩ with HX obtain ⟨U, HU⟩ : (p.norm : ℤ√(-3)) ∣ X := by @@ -206,7 +206,7 @@ theorem Zqrtd.factor_div (a : ℤ√(-3)) {x : ℤ} (hodd : Odd x) : ring _ < x ^ 2 + 3 * x ^ 2 := (add_lt_add ?_ ?_) _ = 4 * x ^ 2 := by ring - + · rw [mul_pow, ← Int.natAbs_pow_two c, ← Int.natAbs_pow_two x, ← mul_pow] norm_cast exact Nat.pow_lt_pow_of_lt_left hc zero_lt_two @@ -313,7 +313,7 @@ theorem factors (a : ℤ√(-3)) (x : ℤ) (hcoprime : IsCoprime a.re a.im) (hod rw [hz, Int.natAbs_mul] exact Nat.le_mul_of_pos_left (pow_pos hgpos 2) _ < x.natAbs := h3 - + · rw [← h6] exact dvd_mul_of_dvd_right hwdvd x #align factors factors @@ -411,7 +411,7 @@ theorem Spts.four {p : ℤ√(-3)} (hfour : p.norm = 4) (hq : p.im ≠ 0) : abs _ = p.norm := by rw [Zsqrtd.norm_def] ring - + · rw [← Int.sub_one_lt_iff, sub_self] exact sq_pos_of_ne_zero _ hq refine' ⟨_, hq⟩ @@ -423,7 +423,7 @@ theorem Spts.four {p : ℤ√(-3)} (hfour : p.norm = 4) (hq : p.im ≠ 0) : abs _ = 1 := by rw [hfour] norm_num - + #align spts.four Spts.four theorem Spts.four_of_coprime {p : ℤ√(-3)} (hcoprime : IsCoprime p.re p.im) (hfour : p.norm = 4) : @@ -433,4 +433,4 @@ theorem Spts.four_of_coprime {p : ℤ√(-3)} (hcoprime : IsCoprime p.re p.im) ( rw [him, isCoprime_zero_right, Int.isUnit_iff_abs_eq] at hcoprime rw [Zsqrtd.norm_def, him, MulZeroClass.mul_zero, sub_zero, ← sq, ← sq_abs, hcoprime] at hfour norm_num at hfour -#align spts.four_of_coprime Spts.four_of_coprime \ No newline at end of file +#align spts.four_of_coprime Spts.four_of_coprime