instCharZero

Mathlib.Algebra.Ring.Nat

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

English

The natural numbers have characteristic zero (the map embedding natural numbers is injective).

Русский

У натуральных чисел характеристика ноль (вставка натуральных чисел инъективна).

LaTeX

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

Lean4

instance instCharZero : CharZero ℕ where cast_injective := Function.injective_id

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

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

Разделы

Аффилиация

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