# 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
• n.succ.unaryCast = n.unaryCast + 1
Instances For
class Nat.AtLeastTwo (n : ) :

A type class for natural numbers which are greater than or equal to 2.

Instances
theorem Nat.AtLeastTwo.prop {n : } [self : n.AtLeastTwo] :
n 2
instance instNatAtLeastTwo {n : } :
(n + 2).AtLeastTwo
Equations
• =
theorem Nat.AtLeastTwo.one_lt {n : } [n.AtLeastTwo] :
1 < n
theorem Nat.AtLeastTwo.ne_one {n : } [n.AtLeastTwo] :
n 1
@[instance 100]
instance instOfNatAtLeastTwo {R : Type u_1} {n : } [] [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 }
@[simp]
theorem Nat.cast_ofNat {R : Type u_1} {n : } [] [n.AtLeastTwo] :
(OfNat.ofNat n) =
theorem Nat.cast_eq_ofNat {R : Type u_1} {n : } [] [n.AtLeastTwo] :
n =

### Additive monoids with one #

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

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

• natCast : 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 : RR
• nsmul_zero : ∀ (x : R), = 0
• nsmul_succ : ∀ (n : ) (x : R), AddMonoid.nsmul (n + 1) x = + x
• one : R
• natCast_zero :

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

• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =

The canonical map ℕ → R is a homomorphism.

Instances
theorem AddMonoidWithOne.natCast_zero {R : Type u_2} [self : ] :

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

theorem AddMonoidWithOne.natCast_succ {R : Type u_2} [self : ] (n : ) :

The canonical map ℕ → R is a homomorphism.

class AddCommMonoidWithOne (R : Type u_2) extends :
Type u_2

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

• natCast : 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 : RR
• nsmul_zero : ∀ (x : R), = 0
• nsmul_succ : ∀ (n : ) (x : R), AddMonoid.nsmul (n + 1) x = + x
• one : R
• natCast_zero :
• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• add_comm : ∀ (a b : R), a + b = b + a

Instances
@[simp]
theorem Nat.cast_zero {R : Type u_1} [] :
0 = 0
theorem Nat.cast_succ {R : Type u_1} [] (n : ) :
n.succ = n + 1
theorem Nat.cast_add_one {R : Type u_1} [] (n : ) :
(n + 1) = n + 1
@[simp]
theorem Nat.cast_ite {R : Type u_1} [] (P : Prop) [] (m : ) (n : ) :
(if P then m else n) = if P then m else n
@[simp]
theorem Nat.cast_one {R : Type u_1} [] :
1 = 1
@[simp]
theorem Nat.cast_add {R : Type u_1} [] (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
• = 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
Instances For
@[simp]
theorem Nat.binCast_eq {R : Type u_1} [] (n : ) :
n.binCast = n
theorem Nat.cast_two {R : Type u_1} [] :
2 = 2
@[reducible, inline]
abbrev AddMonoidWithOne.unary {R : Type u_1} [] [One R] :

AddMonoidWithOne implementation using unary recursion.

Equations
Instances For
@[reducible, inline]
abbrev AddMonoidWithOne.binary {R : Type u_1} [] [One R] :

AddMonoidWithOne implementation using binary recursion.

Equations
Instances For
theorem one_add_one_eq_two {R : Type u_1} [] :
1 + 1 = 2
theorem two_add_one_eq_three {R : Type u_1} [] :
2 + 1 = 3
theorem three_add_one_eq_four {R : Type u_1} [] :
3 + 1 = 4