mathlib3 documentation

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 #

source
@[protected]
def nat.unary_cast {R : Type u} [has_one R] [has_zero R] [has_add R] :
ℕ → R

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

Equations
source
@[class]
structure has_nat_cast (R : Type u) :
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
source
@[instance]
def add_monoid_with_one.to_has_nat_cast (R : Type u) [self : add_monoid_with_one R] :
has_nat_cast R
source
@[class]
structure add_monoid_with_one (R : Type u) :
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
source
@[instance]
def add_monoid_with_one.to_has_one (R : Type u) [self : add_monoid_with_one R] :
has_one R
source
@[instance]
def add_monoid_with_one.to_add_monoid (R : Type u) [self : add_monoid_with_one R] :
add_monoid R
source
@[protected]
def nat.cast {R : Type u} [has_nat_cast R] :
ℕ → R

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

Equations
source
@[instance]
def add_comm_monoid_with_one.to_add_comm_monoid (R : Type u_1) [self : add_comm_monoid_with_one R] :
add_comm_monoid R
source
@[class]
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
source
@[instance]
def add_comm_monoid_with_one.to_add_monoid_with_one (R : Type u_1) [self : add_comm_monoid_with_one R] :
add_monoid_with_one R
source
def library_note.coercion into rings  :
unit

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.

source
@[protected, instance]
def nat.cast_coe {R : Type u_1} [has_nat_cast R] :
has_coe_t ℕ R
Equations
source
@[simp, norm_cast]
theorem nat.cast_zero {R : Type u_1} [add_monoid_with_one R] :
↑0 = 0
source
@[simp, norm_cast]
theorem nat.cast_succ {R : Type u_1} [add_monoid_with_one R] (n : ℕ) :
↑(n.succ) = ↑n + 1
source
theorem nat.cast_add_one {R : Type u_1} [add_monoid_with_one R] (n : ℕ) :
↑(n + 1) = ↑n + 1
source
@[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
source
@[simp, norm_cast]
theorem nat.cast_one {R : Type u_1} [add_monoid_with_one R] :
↑1 = 1
source
@[simp, norm_cast]
theorem nat.cast_add {R : Type u_1} [add_monoid_with_one R] (m n : ℕ) :
↑(m + n) = ↑m + ↑n
source
@[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
source
@[simp]
theorem nat.bin_cast_eq {R : Type u_1} [add_monoid_with_one R] (n : ℕ) :
n.bin_cast = ↑n
source
@[simp, norm_cast]
theorem nat.cast_bit0 {R : Type u_1} [add_monoid_with_one R] (n : ℕ) :
↑(bit0 n) = bit0 ↑n
source
@[simp, norm_cast]
theorem nat.cast_bit1 {R : Type u_1} [add_monoid_with_one R] (n : ℕ) :
↑(bit1 n) = bit1 ↑n
source
theorem nat.cast_two {R : Type u_1} [add_monoid_with_one R] :
↑2 = 2
source
@[protected, reducible]
def add_monoid_with_one.unary {R : Type u_1} [add_monoid R] [has_one R] :
add_monoid_with_one R

add_monoid_with_one implementation using unary recursion.

Equations
source
@[protected, reducible]
def add_monoid_with_one.binary {R : Type u_1} [add_monoid R] [has_one R] :
add_monoid_with_one R

add_monoid_with_one implementation using binary recursion.

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