eq_zero_iff — Mathlib

English

The Jacobi symbol vanishes iff b is nonzero and gcd(a,b) ≠ 1.

Русский

Символ Якоби обнуляется тогда и только тогда, когда b ≠ 0 и gcd(a,b) ≠ 1.

LaTeX

$$$J(a|b) = 0 \iff b \neq 0 \land \gcd(a,b)=1 \text{ не выполняется}\Rightarrow\ g$$$

Lean4

/-- The symbol `J(a | b)` vanishes if and only if `b ≠ 0` and `a` and `b` are not coprime. -/
theorem eq_zero_iff {a : ℤ} {b : ℕ} : J(a | b) = 0 ↔ b ≠ 0 ∧ a.gcd b ≠ 1 :=
  ⟨fun h => by
    rcases eq_or_ne b 0 with hb | hb
    · rw [hb, zero_right] at h; cases h
    exact ⟨hb, mt jacobiSym.ne_zero <| Classical.not_not.2 h⟩, fun ⟨hb, h⟩ => by rw [← neZero_iff] at hb;
    exact eq_zero_iff_not_coprime.2 h⟩

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