instAddMonoidWithOne — Mathlib

English

The natural numbers form an additive monoid with zero and unit 1, using the usual addition.

Русский

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

LaTeX

$$$(\mathbb{N}, +, 0, 1)$ is an additive monoid with one$$

Lean4

instance instAddMonoidWithOne : AddMonoidWithOne ℕ
    where
  natCast n := n
  natCast_zero := rfl
  natCast_succ _ := rfl

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