mathlib documentation


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 #

def nat.unary_cast {R : Type u} [has_one R] [has_zero R] [has_add R] :

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

structure add_monoid_with_one (R : Type u) :

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
  • add_monoid_with_one.has_sizeof_inst
def nat.cast {R : Type u} [has_nat_cast R] :

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

structure add_comm_monoid_with_one (R : Type u_1) :
Type u_1

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
  • add_comm_monoid_with_one.has_sizeof_inst

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] :
@[simp, norm_cast]
theorem nat.cast_zero {R : Type u_1} [add_monoid_with_one R] :
0 = 0
@[simp, norm_cast]
theorem nat.cast_succ {R : Type u_1} [add_monoid_with_one R] (n : ) :
(n.succ) = n + 1
theorem nat.cast_add_one {R : Type u_1} [add_monoid_with_one R] (n : ) :
(n + 1) = n + 1
@[simp, norm_cast]
theorem nat.cast_ite {R : Type u_1} [add_monoid_with_one R] (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} [add_monoid_with_one R] :
1 = 1
@[simp, norm_cast]
theorem nat.cast_add {R : Type u_1} [add_monoid_with_one R] (m n : ) :
(m + n) = m + n
def nat.bin_cast {R : Type u_1} [has_zero R] [has_one R] [has_add R] (n : ) :

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

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

add_monoid_with_one implementation using unary recursion.

@[protected, reducible]

add_monoid_with_one implementation using binary recursion.

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