instNonUnitalNonAssocSemiring — Mathlib

English

The natural numbers can be viewed as a NonUnitalNonAssocSemiring, i.e., with usual addition and multiplication, it satisfies distributivity and has zero as absorbing element, without requiring a unit or multiplication associativity.

Русский

Естественные числа можно рассматривать как NonUnitalNonAssocSemiring, то есть с обычным сложением и умножением, удовлетворяющим распределению и имеющим ноль как поглощающее элемент, без требования единицы или ассоциативности умножения.

LaTeX

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

Lean4

instance instNonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring ℕ
    where
  __ := instAddCommMonoid
  __ := instDistrib
  __ := instMulZeroClass

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