We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 92fe33c commit b249040Copy full SHA for b249040
Mathlib/Algebra/Ring/Int/Parity.lean
@@ -106,7 +106,7 @@ lemma add_one_ediv_two_mul_two_of_odd : Odd n → 1 + n / 2 * 2 = n := by grind
106
107
lemma two_mul_ediv_two_of_odd (h : Odd n) : 2 * (n / 2) = n - 1 := by grind
108
109
-@[simp, grind =]
+@[simp]
110
theorem even_sign_iff {z : ℤ} : Even z.sign ↔ z = 0 := by
111
induction z using wlog_sign with
112
| inv => simp
0 commit comments