mathlib3 documentation

data.int.cast.defs

Cast of integers #

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 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 #

source
@[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
source
@[class]
structure has_int_cast (R : Type u) :
Type u

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
source
@[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
source
@[instance]
def add_group_with_one.to_add_monoid_with_one (R : Type u) [self : add_group_with_one R] :
add_monoid_with_one R
source
@[instance]
def add_group_with_one.to_add_group (R : Type u) [self : add_group_with_one R] :
add_group R
source
@[instance]
def add_group_with_one.to_has_int_cast (R : Type u) [self : add_group_with_one R] :
has_int_cast R
source
@[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
source
@[instance]
def add_comm_group_with_one.to_add_comm_monoid_with_one (R : Type u) [self : add_comm_group_with_one R] :
add_comm_monoid_with_one R
source
@[instance]
def add_comm_group_with_one.to_add_group_with_one (R : Type u) [self : add_comm_group_with_one R] :
add_group_with_one R
source
@[instance]
def add_comm_group_with_one.to_add_comm_group (R : Type u) [self : add_comm_group_with_one R] :
add_comm_group R
source
@[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
source
@[protected, instance]
def int.cast_coe {R : Type u_1} [has_int_cast R] :
has_coe_t ℤ R
Equations
source
theorem int.cast_of_nat {R : Type u} [add_group_with_one R] (n : ℕ) :
↑(int.of_nat n) = ↑n