The natural numbers form an ordered semiring

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

See note [foundational algebra order theory].

Instances

instance Nat.instIsStrictOrderedRing : IsStrictOrderedRing ℕ

@[implicit_reducible]

instance Nat.instLinearOrderedCommMonoidWithZero : LinearOrderedCommMonoidWithZero ℕ

Miscellaneous lemmas

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