exists_nonsquare — Mathlib

English

In a finite field of odd characteristic, there exists a nonsquare element.

Русский

В конечном поле с нечетной характеристикой существует элемент, не являющийся квадратом.

LaTeX

$$$\\\\exists a \\\\in F, \\\\neg IsSquare(a)$$$

Lean4

/-- In a finite field of odd characteristic, not every element is a square. -/
theorem exists_nonsquare (hF : ringChar F ≠ 2) : ∃ a : F, ¬IsSquare a := by
  -- Idea: the squaring map on `F` is not injective, hence not surjective

  have h : ¬Function.Injective fun x : F ↦ x * x := fun h ↦ h.ne (Ring.neg_one_ne_one_of_char_ne_two hF) <| by simp
  simpa [Finite.injective_iff_surjective, Function.Surjective, IsSquare, eq_comm] using h

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