instCharZero

Mathlib.Data.Complex.Basic

URI: https://scilib.ai/kg/mathlib#Complex.instCharZero

English

The complex numbers have characteristic zero: char(ℂ) = 0.

Русский

Комплексные числа имеют характеристику ноль: char(ℂ) = 0.

LaTeX

$$\\operatorname{char}(\\mathbb{C}) = 0$$

Lean4

instance instCharZero : CharZero ℂ :=
  charZero_of_inj_zero fun n h => by rwa [← ofReal_natCast, ofReal_eq_zero, Nat.cast_eq_zero] at h

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

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

Разделы

Аффилиация

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