instCharPOfNatNat

Mathlib.SetTheory.Nimber.Field

URI: https://scilib.ai/kg/mathlib#Nimber.instCharPOfNatNat

English

The nimber type has characteristic 2; i.e., 1 + 1 = 0.

Русский

Тип Nimber имеет характеристику 2; то есть 1 + 1 = 0.

LaTeX

$$$1 + 1 = 0$$$

Lean4

instance : CharP Nimber 2 := by
  apply CharTwo.of_one_ne_zero_of_two_eq_zero one_ne_zero
  rw [← one_add_one_eq_two, add_self]

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

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

Разделы

Аффилиация

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