# 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 intCast : ℤ → R field.

Preferentially, the homomorphism is written as a coercion.

## Main declarations #

• Int.cast: Canonical homomorphism ℤ → R.
• AddGroupWithOne: Type class for Int.cast.
def Int.castDef {R : Type u} [] [Neg R] :
R

Default value for IntCast.intCast in an AddGroupWithOne.

Equations
Instances For

### Additive groups with one #

class AddGroupWithOne (R : Type u) extends , , , :

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

• intCast : R
• natCast : 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 : RR
• nsmul_zero : ∀ (x : R), = 0
• nsmul_succ : ∀ (n : ) (x : R), AddMonoid.nsmul (n + 1) x = + x
• one : R
• natCast_zero :
• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• neg : RR
• sub : RRR
• sub_eq_add_neg : ∀ (a b : R), a - b = a + -b
• zsmul : RR

Multiplication by an integer. Set this to zsmulRec unless Module diamonds are possible.

• zsmul_zero' : ∀ (a : R),
• zsmul_succ' : ∀ (n : ) (a : R), AddGroupWithOne.zsmul (Int.ofNat n.succ) a = + a
• zsmul_neg' : ∀ (n : ) (a : R), = -AddGroupWithOne.zsmul (↑n.succ) a
• neg_add_cancel : ∀ (a : R), -a + a = 0
• intCast_ofNat : ∀ (n : ), = n

The canonical homomorphism ℤ → R agrees with the one from ℕ → R on ℕ.

• intCast_negSucc : ∀ (n : ), = -(n + 1)

The canonical homomorphism ℤ → R for negative values is just the negation of the values of the canonical homomorphism ℕ → R.

Instances
theorem AddGroupWithOne.intCast_ofNat {R : Type u} [self : ] (n : ) :
= n

The canonical homomorphism ℤ → R agrees with the one from ℕ → R on ℕ.

theorem AddGroupWithOne.intCast_negSucc {R : Type u} [self : ] (n : ) :
= -(n + 1)

The canonical homomorphism ℤ → R for negative values is just the negation of the values of the canonical homomorphism ℕ → R.

class AddCommGroupWithOne (R : Type u) extends , , , :

An AddCommGroupWithOne is an AddGroupWithOne satisfying a + b = b + a.

• 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 : RR
• nsmul_zero : ∀ (x : R), = 0
• nsmul_succ : ∀ (n : ) (x : R), AddMonoid.nsmul (n + 1) x = + x
• neg : RR
• sub : RRR
• sub_eq_add_neg : ∀ (a b : R), a - b = a + -b
• zsmul : RR
• zsmul_zero' : ∀ (a : R), = 0
• zsmul_succ' : ∀ (n : ) (a : R), SubNegMonoid.zsmul (Int.ofNat n.succ) a = + a
• zsmul_neg' : ∀ (n : ) (a : R), = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel : ∀ (a : R), -a + a = 0
• add_comm : ∀ (a b : R), a + b = b + a
• intCast : R
• natCast : R
• one : R
• natCast_zero :

The canonical map ℕ → R sends 0 : ℕ to 0 : R.

• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =

The canonical map ℕ → R is a homomorphism.

• intCast_ofNat : ∀ (n : ), = n

The canonical homomorphism ℤ → R agrees with the one from ℕ → R on ℕ.

• intCast_negSucc : ∀ (n : ), = -(n + 1)

The canonical homomorphism ℤ → R for negative values is just the negation of the values of the canonical homomorphism ℕ → R.

Instances