odd_even — Mathlib

Lean4
/-- When `a` is odd and `b` is even, we can replace `b` by `b / 2`. -/
theorem odd_even (a b c : ℕ) (r : ℤ) (ha : a % 2 = 1) (hb : b % 2 = 0) (hc : b / 2 = c) (hr : jacobiSymNat a c = r) :
    jacobiSymNat a b = r :=
  by
  have ha' : legendreSym 2 a = 1 :=
    by
    simp only [legendreSym.mod 2 a, Int.ofNat_mod_ofNat, ha]
    decide
  rcases eq_or_ne c 0 with (rfl | hc')
  · rw [← hr, Nat.eq_zero_of_dvd_of_div_eq_zero (Nat.dvd_of_mod_eq_zero hb) hc]
  · haveI : NeZero c :=
      ⟨hc'⟩
        -- for `jacobiSym.mul_right`

    rwa [← Nat.mod_add_div b 2, hb, hc, Nat.zero_add, jacobiSymNat, jacobiSym.mul_right, ←
      jacobiSym.legendreSym.to_jacobiSym, ha', one_mul]
Похожие утверждения