even_card_of_char_two

Mathlib.FieldTheory.Finite.Basic

URI: https://scilib.ai/kg/mathlib#FiniteField.even_card_of_char_two

English

If the characteristic is 2, then the field has even cardinality.

Русский

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

LaTeX

$$$\\\\text{ringChar}(F) = 2 \\\\Rightarrow \\\\text{card}(F) \\\\equiv 0 \\\\pmod 2$$$

Lean4

theorem even_card_of_char_two (hF : ringChar F = 2) : Fintype.card F % 2 = 0 :=
  even_card_iff_char_two.mp hF

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru