div_four_left — Mathlib

English

If a ≡ 0 mod 4 and b is odd, then J(a/4 | b) = J(a | b).

Русский

Если a ≡ 0 (mod 4) и b нечётно, тогда J(a/4 | b) = J(a | b).

LaTeX

$$$ J(a/4 | b) = J(a | b) $$$

Lean4

theorem div_four_left {a : ℤ} {b : ℕ} (ha4 : a % 4 = 0) (hb2 : b % 2 = 1) : J(a / 4 | b) = J(a | b) :=
  by
  obtain ⟨a, rfl⟩ := Int.dvd_of_emod_eq_zero ha4
  have : Int.gcd (2 : ℕ) b = 1 := by
    rw [Int.gcd_natCast_natCast, ← b.mod_add_div 2, hb2, Nat.gcd_add_mul_left_right, Nat.gcd_one_right]
  rw [Int.mul_ediv_cancel_left _ (by decide), jacobiSym.mul_left, (by decide : (4 : ℤ) = (2 : ℕ) ^ 2),
    jacobiSym.sq_one' this, one_mul]

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