Algebraic order instances for the natural numbers

This file contains algebraic order instances on the natural numbers and a few lemmas about them.

Implementation note

Std has a home-baked development of the algebraic and order theoretic theory of ℕ which, in particular, is not typeclass-mediated. This is useful to set up the algebra and finiteness libraries in mathlib (naturals show up as indices in lists, cardinality in finsets, powers in groups, ...). This home-baked development is pursued in Data.Nat.Defs.

Less basic uses of ℕ should however use the typeclass-mediated development. Data.Nat.Basic gives access to the algebraic instances. The current file is the one giving access to the algebraic order instances.

TODO

The names of this file, Data.Nat.Defs and Data.Nat.Basic are archaic and don't match up with reality anymore. Rename them.

instances

instance Nat.orderBot : OrderBot ℕ

Equations

• Nat.orderBot = OrderBot.mk Nat.zero_le

instance Nat.linearOrderedCommSemiring : LinearOrderedCommSemiring ℕ

Equations

• One or more equations did not get rendered due to their size.

instance Nat.linearOrderedCommMonoidWithZero : LinearOrderedCommMonoidWithZero ℕ

Equations

• One or more equations did not get rendered due to their size.

Extra instances to short-circuit type class resolution and ensure computability

instance Nat.linearOrderedSemiring : LinearOrderedSemiring ℕ

Equations

• Nat.linearOrderedSemiring = inferInstance

instance Nat.strictOrderedSemiring : StrictOrderedSemiring ℕ

Equations

• Nat.strictOrderedSemiring = inferInstance

instance Nat.strictOrderedCommSemiring : StrictOrderedCommSemiring ℕ

Equations

• Nat.strictOrderedCommSemiring = inferInstance

instance Nat.orderedSemiring : OrderedSemiring ℕ

Equations

• Nat.orderedSemiring = StrictOrderedSemiring.toOrderedSemiring'

instance Nat.orderedCommSemiring : OrderedCommSemiring ℕ

Equations

• Nat.orderedCommSemiring = StrictOrderedCommSemiring.toOrderedCommSemiring'

instance Nat.linearOrderedCancelAddCommMonoid : LinearOrderedCancelAddCommMonoid ℕ

Equations

• Nat.linearOrderedCancelAddCommMonoid = inferInstance

instance Nat.canonicallyOrderedCommSemiring : CanonicallyOrderedCommSemiring ℕ

Equations

• One or more equations did not get rendered due to their size.

instance Nat.canonicallyLinearOrderedAddCommMonoid : CanonicallyLinearOrderedAddCommMonoid ℕ

Equations

• One or more equations did not get rendered due to their size.

instance Nat.instOrderedSubNatInstLENatInstAddNatInstSubNat : OrderedSub ℕ

Equations

• Nat.instOrderedSubNatInstLENatInstAddNatInstSubNat = ⋯

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