Commit f939c87 1 parent fc9d94c commit f939c87 Copy full SHA for f939c87
File tree 2 files changed +3
-3
lines changed
2 files changed +3
-3
lines changed Original file line number Diff line number Diff line change @@ -396,7 +396,7 @@ theorem Spts.four {p : ℤ√(-3)} (hfour : p.norm = 4) (hq : p.im ≠ 0) : abs
396
396
ring
397
397
398
398
· rw [← Int.sub_one_lt_iff, sub_self]
399
- exact sq_pos_of_ne_zero _ hq
399
+ exact sq_pos_of_ne_zero hq
400
400
refine' ⟨_, hq⟩
401
401
calc
402
402
p.re ^ 2 = p.re ^ 2 + 3 * p.im ^ 2 - 3 := by simp [hq]
Original file line number Diff line number Diff line change 4
4
[{"url" : " https://github.com/leanprover/std4" ,
5
5
"type" : " git" ,
6
6
"subDir" : null ,
7
- "rev" : " 32983874c1b897d78f20d620fe92fc8fd3f06c3a " ,
7
+ "rev" : " e840c18f7334c751efbd4cfe531476e10c943cdb " ,
8
8
"name" : " std" ,
9
9
"manifestFile" : " lake-manifest.json" ,
10
10
"inputRev" : " main" ,
58
58
{"url" : " https://github.com/leanprover-community/mathlib4.git" ,
59
59
"type" : " git" ,
60
60
"subDir" : null ,
61
- "rev" : " 145460b9327f120bf7013552bb8e8185bd226dea " ,
61
+ "rev" : " cc96d0afe2eefff4ef1ca9e065eed50c34d775c8 " ,
62
62
"name" : " mathlib" ,
63
63
"manifestFile" : " lake-manifest.json" ,
64
64
"inputRev" : null ,
You can’t perform that action at this time.
0 commit comments