even_odd — Mathlib

English

If a is even and b is odd, then the piecewise expression involving J(a/2 | b) equals J(a | b).

Русский

Если a чётно, а b нечётно, то выражение с J(a/2 | b) равно J(a | b).

LaTeX

$$$ (\text{if } b \bmod 8 = 3 \lor b \bmod 8 = 5 \text{ then } -J(a/2 | b) \text{ else } J(a/2 | b)) = J(a | b) $$$

Lean4

theorem even_odd {a : ℤ} {b : ℕ} (ha2 : a % 2 = 0) (hb2 : b % 2 = 1) :
    (if b % 8 = 3 ∨ b % 8 = 5 then -J(a / 2 | b) else J(a / 2 | b)) = J(a | b) :=
  by
  obtain ⟨a, rfl⟩ := Int.dvd_of_emod_eq_zero ha2
  rw [Int.mul_ediv_cancel_left _ (by decide), jacobiSym.mul_left, jacobiSym.at_two (Nat.odd_iff.mpr hb2),
    ZMod.χ₈_nat_eq_if_mod_eight, if_neg (Nat.mod_two_ne_zero.mpr hb2)]
  grind

Похожие утверждения