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

• Nat.instCanonicallyLinearOrderedAddCommMonoid = CanonicallyLinearOrderedAddCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

instance Nat.instLinearOrderedCommMonoid : LinearOrderedCommMonoid ℕ

Equations

• Nat.instLinearOrderedCommMonoid = LinearOrderedCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

instance Nat.instLinearOrderedCancelAddCommMonoid : LinearOrderedCancelAddCommMonoid ℕ

Equations

• Nat.instLinearOrderedCancelAddCommMonoid = LinearOrderedCancelAddCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

theorem Nat.instOrderedSub : OrderedSub ℕ

Miscellaneous lemmas

theorem Nat.pow_left_strictMono {n : ℕ} (hn : n ≠ 0) : StrictMono fun (x : ℕ) => x ^ n

See also pow_left_strictMonoOn₀.

theorem StrictMono.nat_pow {α : Type u_1} {n : ℕ} {f : α → ℕ} [Preorder α] (hn : n ≠ 0) (hf : StrictMono f) : StrictMono fun (x : α) => f x ^ n