Documentation

Mathlib.Algebra.Order.Ring.Nat

The natural numbers form an ordered semiring #

This file contains the commutative linear orderded semiring instance on the natural numbers.

See note [foundational algebra order theory].

Instances #

source
instance Nat.instIsStrictOrderedRing :
IsStrictOrderedRing ℕ
source
instance Nat.instLinearOrderedCommMonoidWithZero :
LinearOrderedCommMonoidWithZero ℕ
Equations

    Miscellaneous lemmas #

    source
    theorem Nat.isCompl_even_odd :
    IsCompl {n : ℕ | Even n} {n : ℕ | Odd n}