Documentation

Mathlib.Algebra.Order.Group.Nat

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 #

Equations
Equations

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