isSquare_of_char_two — Mathlib

English

In a finite field of odd characteristic, not every element is a square.

Русский

В конечном поле с нечетной характеристикой не каждый элемент является квадратом.

LaTeX

$$$\\\\forall F \\\\text{finite}, \\\\text{ringChar}(F) \\\\ne 2 \\\\Rightarrow \\\\exists a \\\\in F, \\\\neg \\\\text{IsSquare}(a)$$$

Lean4

/-- In a finite field of characteristic `2`, all elements are squares. -/
theorem isSquare_of_char_two (hF : ringChar F = 2) (a : F) : IsSquare a :=
  have : CharP F 2 := ringChar.of_eq hF
  isSquare_of_charTwo' a

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