instCommSemiring

Mathlib.Algebra.Ring.Nat

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

English

The natural numbers form a commutative semiring; multiplication is commutative and distributive over addition.

Русский

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

LaTeX

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

Lean4

instance instCommSemiring : CommSemiring ℕ where
  __ := instSemiring
  __ := instCommMonoid

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

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

Разделы

Аффилиация

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