Cast of natural numbers

This file defines the canonical homomorphism from the natural numbers into an AddMonoid with a one. In additive monoids with one, there exists a unique such homomorphism and we store it in the natCast : ℕ → R field.

Preferentially, the homomorphism is written as the coercion Nat.cast.

Main declarations

• NatCast: Type class for Nat.cast.
• AddMonoidWithOne: Type class for which Nat.cast is a canonical monoid homomorphism from ℕ.
• Nat.cast: Canonical homomorphism ℕ → R.

def Nat.unaryCast {R : Type u_1} [One R] [Zero R] [Add R] : ℕ → R

The numeral ((0+1)+⋯)+1.

Equations

• Nat.unaryCast 0 = 0
• n.succ.unaryCast = n.unaryCast + 1

@[instance 100]

instance instOfNatAtLeastTwo {R : Type u_1} {n : ℕ} [NatCast R] [n.AtLeastTwo] : OfNat R n

Recognize numeric literals which are at least 2 as terms of R via Nat.cast. This instance is what makes things like 37 : R type check. Note that 0 and 1 are not needed because they are recognized as terms of R (at least when R is an AddMonoidWithOne) through Zero and One, respectively.

Equations

• instOfNatAtLeastTwo = { ofNat := ↑n }

def Mathlib.LibraryNote.«no_index around OfNat.ofNat» : LibraryNote

When writing lemmas about OfNat.ofNat that assume Nat.AtLeastTwo, the term needs to be wrapped in no_index so as not to confuse simp, as no_index (OfNat.ofNat n).

Rather than referencing this library note, use ofNat(n) as a shorthand for no_index (OfNat.ofNat n).

Some discussion is on Zulip here.

Equations

• Mathlib.LibraryNote.«no_index around OfNat.ofNat» = ()

@[simp]

theorem Nat.cast_ofNat {R : Type u_1} {n : ℕ} [NatCast R] [n.AtLeastTwo] : ↑(OfNat.ofNat n) = OfNat.ofNat n

Additive monoids with one

class AddMonoidWithOne (R : Type u_2) extends NatCast R, AddMonoid R, One R : Type u_2

An AddMonoidWithOne is an AddMonoid with a 1. It also contains data for the unique homomorphism ℕ → R.

• natCast : ℕ → R
• add : R → R → R
• add_assoc (a b c : R) : a + b + c = a + (b + c)
• zero : R
• zero_add (a : R) : 0 + a = a
• add_zero (a : R) : a + 0 = a
• nsmul : ℕ → R → R
• nsmul_zero (x : R) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : R) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• one : R
• natCast_zero : ↑0 = 0

  The canonical map ℕ → R sends 0 : ℕ to 0 : R.

• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1

  The canonical map ℕ → R is a homomorphism.

class AddCommMonoidWithOne (R : Type u_2) extends AddMonoidWithOne R, AddCommMonoid R : Type u_2

An AddCommMonoidWithOne is an AddMonoidWithOne satisfying a + b = b + a.

• natCast : ℕ → R
• add : R → R → R
• add_assoc (a b c : R) : a + b + c = a + (b + c)
• zero : R
• zero_add (a : R) : 0 + a = a
• add_zero (a : R) : a + 0 = a
• nsmul : ℕ → R → R
• nsmul_zero (x : R) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : R) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• one : R
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• add_comm (a b : R) : a + b = b + a

def Mathlib.LibraryNote.«coercion into rings» : LibraryNote

Coercions such as Nat.castCoe that go from a concrete structure such as ℕ to an arbitrary ring R should be set up as follows:

instance : CoeTail ℕ R where coe := ...
instance : CoeHTCT ℕ R where coe := ...

It needs to be CoeTail instead of Coe because otherwise type-class inference would loop when constructing the transitive coercion ℕ → ℕ → ℕ → .... Sometimes we also need to declare the CoeHTCT instance if we need to shadow another coercion (e.g. Nat.cast should be used over Int.ofNat).

Equations

• Mathlib.LibraryNote.«coercion into rings» = ()

@[simp]

theorem Nat.cast_zero {R : Type u_1} [AddMonoidWithOne R] : ↑0 = 0

theorem Nat.cast_succ {R : Type u_1} [AddMonoidWithOne R] (n : ℕ) : ↑n.succ = ↑n + 1

theorem Nat.cast_add_one {R : Type u_1} [AddMonoidWithOne R] (n : ℕ) : ↑(n + 1) = ↑n + 1

@[simp]

theorem Nat.cast_ite {R : Type u_1} [AddMonoidWithOne R] (P : Prop) [Decidable P] (m n : ℕ) : ↑(if P then m else n) = if P then ↑m else ↑n

@[simp]

theorem Nat.cast_one {R : Type u_1} [AddMonoidWithOne R] : ↑1 = 1

@[simp]

theorem Nat.cast_add {R : Type u_1} [AddMonoidWithOne R] (m n : ℕ) : ↑(m + n) = ↑m + ↑n

@[irreducible]

def Nat.binCast {R : Type u_1} [Zero R] [One R] [Add R] : ℕ → R

Computationally friendlier cast than Nat.unaryCast, using binary representation.

Equations

• Nat.binCast 0 = 0
• n.succ.binCast = if (n + 1) % 2 = 0 then ((n + 1) / 2).binCast + ((n + 1) / 2).binCast else ((n + 1) / 2).binCast + ((n + 1) / 2).binCast + 1

@[simp]

theorem Nat.binCast_eq {R : Type u_1} [AddMonoidWithOne R] (n : ℕ) : n.binCast = ↑n

theorem Nat.cast_two {R : Type u_1} [NatCast R] : ↑2 = 2

theorem Nat.cast_three {R : Type u_1} [NatCast R] : ↑3 = 3

theorem Nat.cast_four {R : Type u_1} [NatCast R] : ↑4 = 4

@[reducible, inline]

abbrev AddMonoidWithOne.unary {R : Type u_1} [AddMonoid R] [One R] : AddMonoidWithOne R

AddMonoidWithOne implementation using unary recursion.

Equations

• AddMonoidWithOne.unary = { natCast := Nat.unaryCast, toAddMonoid := inst✝¹, toOne := inst✝, natCast_zero := ⋯, natCast_succ := ⋯ }

@[reducible, inline]

abbrev AddMonoidWithOne.binary {R : Type u_1} [AddMonoid R] [One R] : AddMonoidWithOne R

AddMonoidWithOne implementation using binary recursion.

Equations

• AddMonoidWithOne.binary = { natCast := Nat.binCast, toAddMonoid := inst✝¹, toOne := inst✝, natCast_zero := ⋯, natCast_succ := ⋯ }

theorem one_add_one_eq_two {R : Type u_1} [AddMonoidWithOne R] : 1 + 1 = 2

theorem two_add_one_eq_three {R : Type u_1} [AddMonoidWithOne R] : 2 + 1 = 3

theorem three_add_one_eq_four {R : Type u_1} [AddMonoidWithOne R] : 3 + 1 = 4

theorem two_add_two_eq_four {R : Type u_1} [AddMonoidWithOne R] : 2 + 2 = 4

@[simp]

theorem nsmul_one {A : Type u_2} [AddMonoidWithOne A] (n : ℕ) : n • 1 = ↑n