mathlib documentation

data.int.cast.defs

Cast of integers #

This file defines the canonical homomorphism from the integers into an additive group with a one (typically a ring). In additive groups with a one element, there exists a unique such homomorphism and we store it in the int_cast : ℤ → R field.

Preferentially, the homomorphism is written as a coercion.

Main declarations #

@[protected]
def int.cast_def {R : Type u} [has_nat_cast R] [has_neg R] :
→ R

Default value for add_group_with_one.int_cast.

Equations
@[class]
structure has_int_cast (R : Type u) :
Type u
  • int_cast : → R

Type class for the canonical homomorphism ℤ → R.

Instances of this typeclass
Instances of other typeclasses for has_int_cast
  • has_int_cast.has_sizeof_inst
@[class]
structure add_group_with_one (R : Type u) :
Type u

An add_group_with_one is an add_group with a 1. It also contains data for the unique homomorphisms ℕ → R and ℤ → R.

Instances of this typeclass
Instances of other typeclasses for add_group_with_one
  • add_group_with_one.has_sizeof_inst
@[instance]
@[instance]
@[class]
structure add_comm_group_with_one (R : Type u) :
Type u

An add_comm_group_with_one is an add_group_with_one satisfying a + b = b + a.

Instances of this typeclass
Instances of other typeclasses for add_comm_group_with_one
  • add_comm_group_with_one.has_sizeof_inst
@[protected]
def int.cast {R : Type u} [has_int_cast R] (i : ) :
R

Canonical homomorphism from the integers to any ring(-like) structure R

Equations
@[simp, norm_cast]
theorem nat.cast_sub {R : Type u} [add_group_with_one R] {m n : } (h : m n) :
(n - m) = n - m
@[simp, norm_cast]
theorem nat.cast_pred {R : Type u} [add_group_with_one R] {n : } :
0 < n(n - 1) = n - 1
@[protected, instance]
def int.cast_coe {R : Type u_1} [has_int_cast R] :
Equations
theorem int.cast_of_nat {R : Type u} [add_group_with_one R] (n : ) :
@[simp]
theorem int.cast_neg_succ_of_nat {R : Type u} [add_group_with_one R] (n : ) :
-[1+ n] = -(n + 1)
@[simp, norm_cast]
theorem int.cast_zero {R : Type u} [add_group_with_one R] :
0 = 0
@[simp, norm_cast]
theorem int.cast_coe_nat {R : Type u} [add_group_with_one R] (n : ) :
@[simp, norm_cast]
theorem int.cast_one {R : Type u} [add_group_with_one R] :
1 = 1
@[simp, norm_cast]
theorem int.cast_neg {R : Type u} [add_group_with_one R] (n : ) :
@[simp]
theorem int.cast_sub_nat_nat {R : Type u} [add_group_with_one R] (m n : ) :
@[simp]
theorem int.cast_neg_of_nat {R : Type u} [add_group_with_one R] (n : ) :
@[simp, norm_cast]
theorem int.cast_add {R : Type u} [add_group_with_one R] (m n : ) :
(m + n) = m + n
@[simp, norm_cast]
theorem int.cast_sub {R : Type u} [add_group_with_one R] (m n : ) :
(m - n) = m - n
@[simp, norm_cast]
theorem int.coe_nat_bit0 (n : ) :
@[simp, norm_cast]
theorem int.coe_nat_bit1 (n : ) :
@[simp, norm_cast]
theorem int.cast_bit0 {R : Type u} [add_group_with_one R] (n : ) :
@[simp, norm_cast]
theorem int.cast_bit1 {R : Type u} [add_group_with_one R] (n : ) :
theorem int.cast_two {R : Type u} [add_group_with_one R] :
2 = 2
theorem int.cast_three {R : Type u} [add_group_with_one R] :
3 = 3
theorem int.cast_four {R : Type u} [add_group_with_one R] :
4 = 4