instCharZero

Mathlib.Algebra.Ring.Int.Defs

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

English

ℤ has characteristic zero; the natural embedding from ℕ to ℤ is injective.

Русский

У ℤ характеристика равна нулю; встраивание натуральных чисел ℕ в ℤ инъективно.

LaTeX

$$$\operatorname{CharZero}(\mathbb{Z})$$$

Lean4

instance instCharZero : CharZero ℤ where cast_injective _ _ := ofNat.inj

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

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

Разделы

Аффилиация

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