fix(Tactic.NormNum.LegendreSymbol): not a % 0 but a % 2 (#5719)

leanprover-community · Jul 6, 2023 · 7fe552f · 7fe552f
1 parent ad190bd
commit 7fe552f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/Tactic/NormNum/LegendreSymbol.lean b/Mathlib/Tactic/NormNum/LegendreSymbol.lean
@@ -346,7 +346,7 @@ partial def proveJacobiSymNat (ea eb : Q(ℕ)) : (er : Q(ℤ)) × Q(jacobiSymNat
         show (er : Q(ℤ)) × Q(jacobiSymNat 1 $eb = $er) from
           ⟨mkRawIntLit 1, q(jacobiSymNat.one_left $eb)⟩
       | a =>
-        match a % 0 with
+        match a % 2 with
         | 0 =>
           have hb₀ : Q(Nat.beq ($eb / 2) 0 = false) := (q(Eq.refl false) : Expr)
           have ha : Q(Nat.mod $ea 2 = 0) := (q(Eq.refl 0) : Expr)