odd_card_of_char_ne_two — Mathlib

English

If a finite field has characteristic not equal to 2, its cardinality is odd.

Русский

Если характеристика конечного поля не равна 2, кардинальность поля нечетная.

LaTeX

$$$\\\\text{ringChar}(F) \\\\ne 2 \\\\Rightarrow \\\\text{card}(F) \\\\equiv 1 \\\\pmod 2$$$

Lean4

theorem odd_card_of_char_ne_two (hF : ringChar F ≠ 2) : Fintype.card F % 2 = 1 :=
  Nat.mod_two_ne_zero.mp (mt even_card_iff_char_two.mpr hF)

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