instNonUnitalSemiring

Mathlib.Algebra.Ring.Nat

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

English

The natural numbers form a NonUnitalSemiring, i.e., a semiring without a multiplicative unit.

Русский

Натуральные числа образуют NonUnitalSemiring, то есть полумоной без единицы умножения.

LaTeX

$$$\mathbb{N}$ is a NonUnitalSemiring$$

Lean4

instance instNonUnitalSemiring : NonUnitalSemiring ℕ
    where
  __ := instNonUnitalNonAssocSemiring
  __ := instSemigroupWithZero

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

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

Разделы

Аффилиация

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