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 = ⋯

Miscellaneous lemmas

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

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