even_card_iff_char_two — Mathlib

English

A finite field has even cardinality iff its characteristic is 2.

Русский

Конечное поле имеет чётную кардинальность тогда и только тогда, когда характеристика равна 2.

LaTeX

$$$\\\\text{card}(F) \\\\% 2 = 0 \\\\Leftrightarrow \\\\text{ringChar}(F) = 2$$$

Lean4

/-- The finite field `F` has even cardinality iff it has characteristic `2`. -/
theorem even_card_iff_char_two : ringChar F = 2 ↔ Fintype.card F % 2 = 0 :=
  by
  rcases FiniteField.card F (ringChar F) with ⟨n, hp, h⟩
  rw [h, ← Nat.even_iff, Nat.even_pow, hp.even_iff]
  simp

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