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.instLinearOrderedCommSemiring : LinearOrderedCommSemiring ℕ

Equations

• Nat.instLinearOrderedCommSemiring = LinearOrderedCommSemiring.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

instance Nat.instLinearOrderedCommMonoidWithZero : LinearOrderedCommMonoidWithZero ℕ

Equations

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

instance Nat.instCanonicallyOrderedCommSemiring : CanonicallyOrderedCommSemiring ℕ

Equations

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

Extra instances to short-circuit type class resolution

These also prevent non-computable instances being used to construct these instances non-computably.

instance Nat.instLinearOrderedSemiring : LinearOrderedSemiring ℕ

Equations

• Nat.instLinearOrderedSemiring = inferInstance

instance Nat.instStrictOrderedSemiring : StrictOrderedSemiring ℕ

Equations

• Nat.instStrictOrderedSemiring = inferInstance

instance Nat.instStrictOrderedCommSemiring : StrictOrderedCommSemiring ℕ

Equations

• Nat.instStrictOrderedCommSemiring = inferInstance

instance Nat.instOrderedSemiring : OrderedSemiring ℕ

Equations

• Nat.instOrderedSemiring = StrictOrderedSemiring.toOrderedSemiring'

instance Nat.instOrderedCommSemiring : OrderedCommSemiring ℕ

Equations

• Nat.instOrderedCommSemiring = StrictOrderedCommSemiring.toOrderedCommSemiring'

Miscellaneous lemmas

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