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} [One R] [Zero R] [Add R] : ℕ → R

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

Equations

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

class Nat.AtLeastTwo (n : ℕ) : Prop

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

• prop : n ≥ 2

instance instNatAtLeastTwo {n : ℕ} : Nat.AtLeastTwo (n + 2)

Equations

• ⋯ = ⋯

theorem Nat.AtLeastTwo.one_lt {n : ℕ} [Nat.AtLeastTwo n] : 1 < n

theorem Nat.AtLeastTwo.ne_one {n : ℕ} [Nat.AtLeastTwo n] : n ≠ 1

instance instOfNatAtLeastTwo {R : Type u_1} {n : ℕ} [NatCast R] [Nat.AtLeastTwo n] : 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 : ℕ} [NatCast R] [Nat.AtLeastTwo n] : ↑(OfNat.ofNat n) = OfNat.ofNat n

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

Additive monoids with one

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

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 : NatCast.natCast 0 = 0

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

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

  The canonical map ℕ → R is a homomorphism.

class AddCommMonoidWithOne (R : Type u_1) extends AddMonoidWithOne : Type u_1

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 : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• add_comm : ∀ (a b : R), a + b = b + a

  Addition is commutative in an commutative additive magma.

@[simp]

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

@[simp]

theorem Nat.cast_succ {R : Type u_1} [AddMonoidWithOne R] (n : ℕ) : ↑(Nat.succ n) = ↑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

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
• Nat.binCast (Nat.succ n) = if (n + 1) % 2 = 0 then Nat.binCast ((n + 1) / 2) + Nat.binCast ((n + 1) / 2) else Nat.binCast ((n + 1) / 2) + Nat.binCast ((n + 1) / 2) + 1

@[simp]

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

@[deprecated]

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

@[deprecated]

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

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

@[reducible]

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

AddMonoidWithOne implementation using unary recursion.

Equations

• AddMonoidWithOne.unary = let __src := inst; let __src_1 := inst✝; AddMonoidWithOne.mk ⋯ ⋯

@[reducible]

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

AddMonoidWithOne implementation using binary recursion.

Equations

• AddMonoidWithOne.binary = let __src := inst; let __src_1 := inst✝; AddMonoidWithOne.mk ⋯ ⋯

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

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

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