The naturals form a linear ordered monoid

This file contains the linear ordered monoid instance on the natural numbers.

See note [foundational algebra order theory].

Instances

instance Nat.instCanonicallyLinearOrderedAddCommMonoid : CanonicallyLinearOrderedAddCommMonoid ℕ

Equations

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

instance Nat.instLinearOrderedCommMonoid : LinearOrderedCommMonoid ℕ

Equations

• Nat.instLinearOrderedCommMonoid = let __spread.0 := Nat.instLinearOrder; LinearOrderedCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

instance Nat.instLinearOrderedCancelAddCommMonoid : LinearOrderedCancelAddCommMonoid ℕ

Equations

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

instance Nat.instOrderedSub : OrderedSub ℕ

Equations

• Nat.instOrderedSub = ⋯

Extra instances to short-circuit type class resolution

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

instance Nat.instOrderBot : OrderBot ℕ

Equations

• Nat.instOrderBot = inferInstance

Miscellaneous lemmas

theorem NeZero.one_le {n : ℕ} [NeZero n] : 1 ≤ n