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
- One or more equations did not get rendered due to their size.
Equations
- Nat.instLinearOrderedCommMonoid = let __spread.0 := Nat.instLinearOrder; LinearOrderedCommMonoid.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯
Equations
- One or more equations did not get rendered due to their size.
Miscellaneous lemmas #
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