# 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`.

source
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

Instances For

source
@[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 }

source
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» = ()

Instances For

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

### Additive monoids with one #

source
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.

Instances

source
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

Instances

source
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» = ()

Instances For

source
@[simp]
theorem Nat.cast_zero {R : Type u_1} [AddMonoidWithOne R] :
↑0 = 0
source
theorem Nat.cast_succ {R : Type u_1} [AddMonoidWithOne R] (n : ℕ) :
↑n.succ = ↑n + 1
source
theorem Nat.cast_add_one {R : Type u_1} [AddMonoidWithOne R] (n : ℕ) :
↑(n + 1) = ↑n + 1
source
@[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
source
@[simp]
theorem Nat.cast_one {R : Type u_1} [AddMonoidWithOne R] :
↑1 = 1
source
@[simp]
theorem Nat.cast_add {R : Type u_1} [AddMonoidWithOne R] (m n : ℕ) :
↑(m + n) = ↑m + ↑n
source
@[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

Instances For

source
@[simp]
theorem Nat.binCast_eq {R : Type u_1} [AddMonoidWithOne R] (n : ℕ) :
n.binCast = ↑n
source
theorem Nat.cast_two {R : Type u_1} [NatCast R] :
↑2 = 2
source
theorem Nat.cast_three {R : Type u_1} [NatCast R] :
↑3 = 3
source
theorem Nat.cast_four {R : Type u_1} [NatCast R] :
↑4 = 4
source
@[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 := ⋯ }

Instances For

source
@[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 := ⋯ }

Instances For

source
theorem one_add_one_eq_two {R : Type u_1} [AddMonoidWithOne R] :
1 + 1 = 2
source
theorem two_add_one_eq_three {R : Type u_1} [AddMonoidWithOne R] :
2 + 1 = 3
source
theorem three_add_one_eq_four {R : Type u_1} [AddMonoidWithOne R] :
3 + 1 = 4
source
theorem two_add_two_eq_four {R : Type u_1} [AddMonoidWithOne R] :
2 + 2 = 4
source
@[simp]
theorem nsmul_one {A : Type u_2} [AddMonoidWithOne A] (n : ℕ) :
n • 1 = ↑n