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.instIsOrderedAddMonoid : IsOrderedAddMonoid ℕ

instance Nat.instIsOrderedCancelAddMonoid : IsOrderedCancelAddMonoid ℕ

instance Nat.instCanonicallyOrderedAdd : CanonicallyOrderedAdd ℕ

instance 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