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

instance Nat.instIsStrictOrderedRing : IsStrictOrderedRing ℕ

instance Nat.instLinearOrderedCommMonoidWithZero : LinearOrderedCommMonoidWithZero ℕ

Equations

• One or more equations did not get rendered due to their size.

Miscellaneous lemmas

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