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

class Nat.AtLeastTwo (n : ℕ) :

Prop

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

prop : n ≥ 2

Instances

source

theorem Nat.AtLeastTwo.prop {n : ℕ} [self : n.AtLeastTwo] :

n ≥ 2

source

instance instNatAtLeastTwo {n : ℕ} :

(n + 2).AtLeastTwo

Equations

⋯ = ⋯

source

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

1 < n

source

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

n ≠ 1

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

@[simp]

theorem Nat.cast_ofNat {R : Type u_1} {n : ℕ} [NatCast R] [n.AtLeastTwo] :

↑(OfNat.ofNat n) = OfNat.ofNat n

source

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

↑n = OfNat.ofNat n

Additive monoids with one #

source

class AddMonoidWithOne (R : Type u_2) extends NatCast , AddMonoid , One , AddSemigroup , AddZeroClass , Zero , Add :

Type u_2

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

Instances

source

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

NatCast.natCast 0 = 0

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

source

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

NatCast.natCast (n + 1) = NatCast.natCast n + 1

The canonical map ℕ → R is a homomorphism.

source

class AddCommMonoidWithOne (R : Type u_2) extends AddMonoidWithOne , AddCommMonoid , NatCast , AddMonoid , One , AddCommSemigroup , AddSemigroup , AddZeroClass , Zero , AddCommMagma , Add :

Type u_2

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

Instances

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