eq_one_or_neg_one — Mathlib

English

Let a ∈ ℤ and b ∈ ℕ with gcd(a,b) = 1. Then the Jacobi symbol J(a | b) takes the values ±1.

Русский

Пусть a ∈ ℤ и b ∈ ℕ, причём gcd(a,b) = 1. Тогда символ Якоби J(a | b) принимает значения ±1.

LaTeX

$$$ J(a \;|\; b) = 1 \\lor J(a \;|\; b) = -1 $$$

Lean4

/-- The symbol `J(a | b)` takes the value `1` or `-1` if `a` and `b` are coprime. -/
theorem eq_one_or_neg_one {a : ℤ} {b : ℕ} (h : a.gcd b = 1) : J(a | b) = 1 ∨ J(a | b) = -1 :=
  (trichotomy a b).resolve_left <| jacobiSym.ne_zero h

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