eq_neg_one_iff_not_one — Mathlib

English

For prime p and a ∈ ℤ with a ≠ 0 mod p, legendreSym p a = -1 iff legendreSym p a ≠ 1.

Русский

Для простого p и целого a, не делящегося на p, legendreSym p a = -1 тогда и только тогда, когда legendreSym p a не равно 1.

LaTeX

$$$\mathrm{legendreSym}(p,a) = -1 \iff \lnot (\mathrm{legendreSym}(p,a) = 1)$$$

Lean4

theorem eq_neg_one_iff_not_one {a : ℤ} (ha : (a : ZMod p) ≠ 0) : legendreSym p a = -1 ↔ ¬legendreSym p a = 1 :=
  quadraticChar_eq_neg_one_iff_not_one ha

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