doc-next-gen

Mathlib.Algebra.Order.Ring.Nat

Module docstring

{"# The natural numbers form an ordered semiring

This file contains the commutative linear orderded semiring instance on the natural numbers.

See note [foundational algebra order theory]. ","### Instances ","### Miscellaneous lemmas "}

Nat.instIsStrictOrderedRing instance
: IsStrictOrderedRing ℕ
Full source 
instance instIsStrictOrderedRing : IsStrictOrderedRing ℕ where
  add_le_add_left := @Nat.add_le_add_left
  le_of_add_le_add_left := @Nat.le_of_add_le_add_left
  zero_le_one := Nat.le_of_lt (Nat.zero_lt_succ 0)
  mul_lt_mul_of_pos_left := @Nat.mul_lt_mul_of_pos_left
  mul_lt_mul_of_pos_right := @Nat.mul_lt_mul_of_pos_right
  exists_pair_ne := ⟨0, 1, ne_of_lt Nat.zero_lt_one⟩
Natural Numbers as a Strict Ordered Semiring
Informal description
The natural numbers $\mathbb{N}$ form a strict ordered semiring with the usual order and operations.
Nat.instLinearOrderedCommMonoidWithZero instance
: LinearOrderedCommMonoidWithZero ℕ
Full source 
instance instLinearOrderedCommMonoidWithZero : LinearOrderedCommMonoidWithZero ℕ where
  zero_le_one := zero_le_one
  mul_le_mul_left _ _ h c := Nat.mul_le_mul_left c h
Natural Numbers as a Linearly Ordered Commutative Monoid with Zero
Informal description
The natural numbers $\mathbb{N}$ form a linearly ordered commutative monoid with zero, where the order is compatible with the monoid operation and zero is the least element.