mathlib documentation

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 #

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

Default value for add_group_with_one.int_cast.

structure add_group_with_one (R : 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
structure add_comm_group_with_one (R : 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
def int.cast {R : Type u} [has_int_cast R] (i : ) :

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

@[protected, instance]
def int.cast_coe {R : Type u_1} [has_int_cast R] :
theorem int.cast_of_nat {R : Type u} [add_group_with_one R] (n : ) :