mathlib3documentation

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 #

• int.cast: Canonical homomorphism ℤ → R.
• add_group_with_one: Type class for int.cast.
@[protected]
def int.cast_def {R : Type u} [has_nat_cast R] [has_neg R] :

Default value for add_group_with_one.int_cast.

Equations
@[class]
structure has_int_cast (R : 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
@[class]
structure add_group_with_one (R : Type u) :
• int_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"
• neg : R R
• sub : R R R
• sub_eq_add_neg : ( (a b : R), a - b = a + -b) . "try_refl_tac"
• zsmul : R R
• zsmul_zero' : ( (a : R), . "try_refl_tac"
• zsmul_succ' : ( (n : ) (a : R), = a + . "try_refl_tac"
• zsmul_neg' : ( (n : ) (a : R), . "try_refl_tac"
• add_left_neg : (a : R), -a + a = 0
• nat_cast : R
• one : R
• nat_cast_zero : . "control_laws_tac"
• nat_cast_succ : ( (n : ), . "control_laws_tac"
• int_cast_of_nat : ( (n : ), . "control_laws_tac"
• int_cast_neg_succ_of_nat : ( (n : ), add_group_with_one.int_cast (-(n + 1)) = -(n + 1)) . "control_laws_tac"

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
@[instance]
@[instance]
@[class]
structure add_comm_group_with_one (R : Type u) :
• 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"
• neg : R R
• sub : R R R
• sub_eq_add_neg : ( (a b : R), a - b = a + -b) . "try_refl_tac"
• zsmul : R R
• zsmul_zero' : ( (a : R), . "try_refl_tac"
• zsmul_succ' : ( (n : ) (a : R), . "try_refl_tac"
• zsmul_neg' : ( (n : ) (a : R), . "try_refl_tac"
• add_left_neg : (a : R), -a + a = 0
• add_comm : (a b : R), a + b = b + a
• int_cast : R
• nat_cast : R
• one : R
• nat_cast_zero : . "control_laws_tac"
• nat_cast_succ : ( (n : ), . "control_laws_tac"
• int_cast_of_nat : ( (n : ), . "control_laws_tac"
• int_cast_neg_succ_of_nat : ( (n : ), = -(n + 1)) . "control_laws_tac"

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
Canonical homomorphism from the integers to any ring(-like) structure R