quadraticChar_eq_pow_of_char_ne_two

English

If ringChar F ≠ 2 and a ≠ 0, then χF(a) equals 1 when a^{|F|/2} = 1 and −1 otherwise.

Русский

Если ringChar F ≠ 2 и a ≠ 0, то χF(a) = 1, когда a^{|F|/2} = 1, иначе χF(a) = −1.

LaTeX

$$$\text{If } \operatorname{ringChar}(F) \neq 2\text{ and } a \neq 0,\; χ_F(a) = \begin{cases}1,& a^{|F|/2}=1\\-1,& \text{otherwise}\end{cases}$$$

Lean4

/-- If `ringChar F` is odd, then `quadraticChar F a` can be computed in
terms of `a ^ (Fintype.card F / 2)`. -/
theorem quadraticChar_eq_pow_of_char_ne_two (hF : ringChar F ≠ 2) {a : F} (ha : a ≠ 0) :
    quadraticChar F a = if a ^ (Fintype.card F / 2) = 1 then 1 else -1 :=
  quadraticCharFun_eq_pow_of_char_ne_two hF ha

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