instSemiring — Mathlib

English

The natural numbers form a Semiring, i.e., they have additive and multiplicative structures with distributive laws and identity elements 0 and 1.

Русский

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

LaTeX

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

Lean4

instance instSemiring : Semiring ℕ where
  __ := instNonUnitalSemiring
  __ := instNonAssocSemiring
  __ := instMonoidWithZero

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