mathlib3documentation

data.nat.cast.defs

Cast of natural numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Preferentially, the homomorphism is written as a coercion.

Main declarations #

• add_monoid_with_one: Type class for nat.cast.
• nat.cast: Canonical homomorphism ℕ → R.
@[protected]
def nat.unary_cast {R : Type u} [has_one R] [has_zero R] [has_add R] :

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

Equations
@[class]
structure has_nat_cast (R : Type u) :

Type class for the canonical homomorphism ℕ → R.

Instances of this typeclass
Instances of other typeclasses for has_nat_cast
• has_nat_cast.has_sizeof_inst
@[instance]
@[class]
structure add_monoid_with_one (R : Type u) :
• nat_cast : 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), . "try_refl_tac"
• nsmul_succ' : ( (n : ) (x : R), . "try_refl_tac"
• one : R
• nat_cast_zero : . "control_laws_tac"
• nat_cast_succ : ( (n : ), . "control_laws_tac"

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

Instances of this typeclass
Instances of other typeclasses for add_monoid_with_one
@[instance]
@[instance]
@[protected]
def nat.cast {R : Type u} [has_nat_cast R] :

Canonical homomorphism from ℕ to a additive monoid R with a 1.

Equations
@[class]
structure add_comm_monoid_with_one (R : Type u_1) :
Type u_1
• nat_cast : 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), . "try_refl_tac"
• nsmul_succ' : ( (n : ) (x : R), . "try_refl_tac"
• one : R
• nat_cast_zero : . "control_laws_tac"
• nat_cast_succ : ( (n : ), . "control_laws_tac"
• add_comm : (a b : R), a + b = b + a

An add_comm_monoid_with_one is an add_monoid_with_one satisfying a + b = b + a.

Instances of this typeclass
Instances of other typeclasses for add_comm_monoid_with_one

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

@[priority 900] instance : has_coe_t ℕ R := ⟨...⟩


It needs to be has_coe_t instead of has_coe because otherwise type-class inference would loop when constructing the transitive coercion ℕ → ℕ → ℕ → .... The reduced priority is necessary so that it doesn't conflict with instances such as has_coe_t R (option R).

For this to work, we reduce the priority of the coe_base and coe_trans instances because we want the instances for has_coe_t to be tried in the following order:

1. has_coe_t instances declared in mathlib (such as has_coe_t R (with_top R), etc.)
2. coe_base, which contains instances such as has_coe (fin n) n
3. nat.cast_coe : has_coe_t ℕ R etc.
4. coe_trans

If coe_trans is tried first, then nat.cast_coe doesn't get a chance to apply.

@[protected, instance]
def nat.cast_coe {R : Type u_1} [has_nat_cast R] :
Equations
@[simp, norm_cast]
theorem nat.cast_zero {R : Type u_1}  :
0 = 0
@[simp, norm_cast]
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, norm_cast]
theorem nat.cast_ite {R : Type u_1} (P : Prop) [decidable P] (m n : ) :
(ite P m n) = ite P m n
@[simp, norm_cast]
theorem nat.cast_one {R : Type u_1}  :
1 = 1
@[simp, norm_cast]
theorem nat.cast_add {R : Type u_1} (m n : ) :
(m + n) = m + n
@[protected]
def nat.bin_cast {R : Type u_1} [has_zero R] [has_one R] [has_add R] (n : ) :
R

Computationally friendlier cast than nat.unary_cast, using binary representation.

Equations
@[simp]
theorem nat.bin_cast_eq {R : Type u_1} (n : ) :
@[simp, norm_cast]
theorem nat.cast_bit0 {R : Type u_1} (n : ) :
(bit0 n) =
@[simp, norm_cast]
theorem nat.cast_bit1 {R : Type u_1} (n : ) :
(bit1 n) =
theorem nat.cast_two {R : Type u_1}  :
2 = 2
@[protected, reducible]

add_monoid_with_one implementation using unary recursion.

Equations
@[protected, reducible]

add_monoid_with_one implementation using binary recursion.

Equations
theorem ne_zero.nat_cast_ne (n : ) (R : Type u_1) [h : ne_zero n] :
n 0
theorem ne_zero.of_ne_zero_coe (R : Type u_1) {n : } [h : ne_zero n] :
theorem ne_zero.pos_of_ne_zero_coe (R : Type u_1) {n : } [ne_zero n] :
0 < n