English
In any semigroup, multiplication is associative: a·(b·c) = (a·b)·c for all a,b,c.
Русский
В произвольном полугруппе умножение ассоциативно: a·(b·c) = (a·b)·c для всех a,b,c.
LaTeX
$$$\forall G \; [\text{Semigroup } G],\forall a,b,c \in G,\ a \cdot (b \cdot c) = (a \cdot b) \cdot c$$$
Lean4
/-- The Jacobi symbol `J(a | b)` depends only on `b` mod `4*a` (version for `a : ℕ`). -/
theorem mod_right' (a : ℕ) {b : ℕ} (hb : Odd b) : J(a | b) = J(a | b % (4 * a)) :=
by
rcases eq_or_ne a 0 with (rfl | ha₀)
· rw [mul_zero, mod_zero]
have hb' : Odd (b % (4 * a)) := hb.mod_even (Even.mul_right (by decide) _)
rcases exists_eq_pow_mul_and_not_dvd ha₀ 2 (by simp) with ⟨e, a', ha₁', ha₂⟩
have ha₁ := odd_iff.mpr (two_dvd_ne_zero.mp ha₁')
nth_rw 2 [ha₂]; nth_rw 1 [ha₂]
rw [Nat.cast_mul, mul_left, mul_left, quadratic_reciprocity' ha₁ hb, quadratic_reciprocity' ha₁ hb', Nat.cast_pow,
pow_left, pow_left, Nat.cast_two, at_two hb, at_two hb']
congr 1; swap
· congr 1
· simp_rw [qrSign]
rw [χ₄_nat_mod_four, χ₄_nat_mod_four (b % (4 * a)), mod_mod_of_dvd b (dvd_mul_right 4 a)]
· rw [mod_left ↑(b % _), mod_left b, Int.natCast_mod, Int.emod_emod_of_dvd b]
simp only [ha₂, Nat.cast_mul, ← mul_assoc]
apply dvd_mul_left
rcases e with - | e; · rfl
· rw [χ₈_nat_mod_eight, χ₈_nat_mod_eight (b % (4 * a)), mod_mod_of_dvd b]
use 2 ^ e * a'; rw [ha₂, Nat.pow_succ]; ring
