eq_zero_iff_not_coprime — Mathlib

English

The Jacobi symbol is multiplicative in its first argument: J(a1*a2 | b) = J(a1|b) J(a2|b).

Русский

Символ Якоби мультипликативен по первому аргументу: J(a1*a2 | b) = J(a1 | b) J(a2 | b).

LaTeX

$$$J(a_1 a_2 \mid b) = J(a_1 \mid b) \cdot J(a_2 \mid b)$$$

Lean4

/-- The symbol `J(a | b)` vanishes iff `a` and `b` are not coprime (assuming `b ≠ 0`). -/
theorem eq_zero_iff_not_coprime {a : ℤ} {b : ℕ} [NeZero b] : J(a | b) = 0 ↔ a.gcd b ≠ 1 :=
  List.prod_eq_zero_iff.trans
    (by
      rw [List.mem_pmap, Int.gcd_eq_natAbs, Ne, Prime.not_coprime_iff_dvd]
      simp_rw [legendreSym.eq_zero_iff _ _, intCast_zmod_eq_zero_iff_dvd, mem_primeFactorsList (NeZero.ne b), ←
        Int.natCast_dvd, Int.natCast_dvd_natCast, exists_prop, and_assoc, _root_.and_comm])

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