eq_one_of_sq_sub_mul_sq_eq_zero' — Mathlib

English

The Legendre symbol defines a monoid-with-zero hom from ℤ to ℤ with toFun = legendreSym p.

Русский

Символ Лежандра задаёт гомоморфизм моноида с нулём из целых чисел в целые числа, отображение задано как legendreSym p.

LaTeX

$$$\mathrm{hom}: \mathbb{Z} \to_{\text{MonoidWithZero}} \mathbb{Z},\; \mathrm{toFun}=\mathrm{legendreSym}(p)$$$

Lean4

/-- The Legendre symbol `legendreSym p a = 1` if there is a solution in `ℤ/pℤ`
of the equation `x^2 - a*y^2 = 0` with `x ≠ 0`. -/
theorem eq_one_of_sq_sub_mul_sq_eq_zero' {p : ℕ} [Fact p.Prime] {a : ℤ} (ha : (a : ZMod p) ≠ 0) {x y : ZMod p}
    (hx : x ≠ 0) (hxy : x ^ 2 - a * y ^ 2 = 0) : legendreSym p a = 1 :=
  by
  haveI hy : y ≠ 0 := by
    rintro rfl
    rw [zero_pow two_ne_zero, mul_zero, sub_zero, sq_eq_zero_iff] at hxy
    exact hx hxy
  exact eq_one_of_sq_sub_mul_sq_eq_zero ha hy hxy

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