quadraticCharFun_eq_pow_of_char_ne_two

English

If the characteristic is odd, then quadraticCharFun F a equals 1 if a^(|F|/2) = 1, otherwise -1, provided a ≠ 0.

Русский

Если характеристика поля F не равна 2, то квадратичный характер F действует так: он равен 1, если a^(|F|/2) = 1, иначе -1, при a ≠ 0.

LaTeX

$$$\text{quadraticCharFun } F a = \begin{cases}1,& a^{|F|/2}=1, \\ -1,& \text{иначе} \end{cases}$ при $\text{ringChar } F \neq 2$ и $a \neq 0$$$

Lean4

/-- If `ringChar F` is odd, then `quadraticCharFun F a` can be computed in
terms of `a ^ (Fintype.card F / 2)`. -/
theorem quadraticCharFun_eq_pow_of_char_ne_two (hF : ringChar F ≠ 2) {a : F} (ha : a ≠ 0) :
    quadraticCharFun F a = if a ^ (Fintype.card F / 2) = 1 then 1 else -1 :=
  by
  simp only [quadraticCharFun, ha, if_false]
  simp_rw [FiniteField.isSquare_iff hF ha]

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