nonsquare_of_jacobiSym_eq_neg_one

English

If J(a | b) = -1, then a is not a square modulo b.

Русский

Если J(a | b) = -1, то a не является квадратом по модулю b.

LaTeX

$$$ J(a | b) = -1 \Rightarrow \neg IsSquare (a \bmod b) $$$

Lean4

/-- If `J(a | b)` is `-1`, then `a` is not a square modulo `b`. -/
theorem nonsquare_of_jacobiSym_eq_neg_one {a : ℤ} {b : ℕ} (h : J(a | b) = -1) : ¬IsSquare (a : ZMod b) := fun ⟨r, ha⟩ =>
  by
  rw [← r.coe_valMinAbs, ← Int.cast_mul, intCast_eq_intCast_iff', ← sq] at ha
  apply (by simp : ¬(0 : ℤ) ≤ -1)
  rw [← h, mod_left, ha, ← mod_left, pow_left]
  apply sq_nonneg

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