Update Reductions.lean

Co-Authored-By: Yaël Dillies <[email protected]>
ImperialCollegeLondon · Nov 10, 2024 · d33b528 · d33b528
1 parent 64abeb0
commit d33b528
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/FLT/Basic/Reductions.lean b/FLT/Basic/Reductions.lean
@@ -256,8 +256,8 @@ lemma FreyCurve.j (P : FreyPackage) :
 private lemma j_pos_aux (a b : ℤ) (hb : b ≠ 0) : 0 < (a + b) ^ 2 - a * b := by
   rify
   calc
-      (0 : ℝ) < (a ^ 2 + (a + b) ^ 2 + b ^ 2) / 2 := by positivity
-      _ = (a + b) ^ 2 - a * b := by ring
+    (0 : ℝ) < (a ^ 2 + (a + b) ^ 2 + b ^ 2) / 2 := by positivity
+    _ = (a + b) ^ 2 - a * b := by ring
 
 /-- The q-adic valuation of the j-invariant of the Frey curve is a multiple of p if 2 < q is
 a prime of bad reduction. -/