Algebraic instances for the natural numbers

This file contains algebraic 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. This file is the one giving access to the algebraic instances. Data.Nat.Order.Basic is the one giving access to the algebraic order instances.

TODO

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

Instances

instance Nat.commSemiring : CommSemiring ℕ

Equations

• Nat.commSemiring = CommSemiring.mk Nat.mul_comm

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

instance Nat.addCommMonoid : AddCommMonoid ℕ

Equations

• Nat.addCommMonoid = inferInstance

instance Nat.addMonoid : AddMonoid ℕ

Equations

• Nat.addMonoid = inferInstance

instance Nat.monoid : Monoid ℕ

Equations

• Nat.monoid = inferInstance

instance Nat.commMonoid : CommMonoid ℕ

Equations

• Nat.commMonoid = inferInstance

instance Nat.commSemigroup : CommSemigroup ℕ

Equations

• Nat.commSemigroup = inferInstance

instance Nat.semigroup : Semigroup ℕ

Equations

• Nat.semigroup = inferInstance

instance Nat.addCommSemigroup : AddCommSemigroup ℕ

Equations

• Nat.addCommSemigroup = inferInstance

instance Nat.addSemigroup : AddSemigroup ℕ

Equations

• Nat.addSemigroup = inferInstance

instance Nat.distrib : Distrib ℕ

Equations

• Nat.distrib = inferInstance

instance Nat.semiring : Semiring ℕ

Equations

• Nat.semiring = inferInstance

instance Nat.cancelCommMonoidWithZero : CancelCommMonoidWithZero ℕ

Equations

• Nat.cancelCommMonoidWithZero = let __src := inferInstance; CancelCommMonoidWithZero.mk

Extra lemmas

theorem Nat.nsmul_eq_mul (m : ℕ) (n : ℕ) : m • n = m * n

theorem Nat.toAdd_pow (a : Multiplicative ℕ) (b : ℕ) : Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * b

@[simp]

theorem Nat.ofAdd_mul (a : ℕ) (b : ℕ) : Multiplicative.ofAdd (a * b) = Multiplicative.ofAdd a ^ b