Basic instances for the natural numbers

This file contains:

• Algebraic instances on the natural numbers
• Basic lemmas about natural numbers that require more imports than available in Data.Nat.Defs.

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