From f939c87a86597b9032de8e9f3f6e027a16f131d6 Mon Sep 17 00:00:00 2001 From: riccardobrasca Date: Mon, 22 Apr 2024 03:55:56 +0200 Subject: [PATCH] bump --- FltRegular/FltThree/Spts.lean | 2 +- lake-manifest.json | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/FltRegular/FltThree/Spts.lean b/FltRegular/FltThree/Spts.lean index 93f285ce..524f6927 100644 --- a/FltRegular/FltThree/Spts.lean +++ b/FltRegular/FltThree/Spts.lean @@ -396,7 +396,7 @@ theorem Spts.four {p : ℤ√(-3)} (hfour : p.norm = 4) (hq : p.im ≠ 0) : abs ring · rw [← Int.sub_one_lt_iff, sub_self] - exact sq_pos_of_ne_zero _ hq + exact sq_pos_of_ne_zero hq refine' ⟨_, hq⟩ calc p.re ^ 2 = p.re ^ 2 + 3 * p.im ^ 2 - 3 := by simp [hq] diff --git a/lake-manifest.json b/lake-manifest.json index 654639f1..a6adbefa 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover/std4", "type": "git", "subDir": null, - "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a", + "rev": "e840c18f7334c751efbd4cfe531476e10c943cdb", "name": "std", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,7 +58,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "145460b9327f120bf7013552bb8e8185bd226dea", + "rev": "cc96d0afe2eefff4ef1ca9e065eed50c34d775c8", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,