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

source
def Int.castDef {R : Type u} [NatCast R] [Neg R] :
ℤ → R

Default value for `IntCast.intCast` in an `AddGroupWithOne`.

Equations

- (Int.ofNat n).castDef = ↑n
- (Int.negSucc n).castDef = -↑(n + 1)

Instances For

### Additive groups with one #

source
class AddGroupWithOne (R : Type u) extends IntCast R, AddMonoidWithOne R, AddGroup R :
Type u

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

- intCast : ℤ → R
- natCast : ℕ → 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) : AddMonoid.nsmul 0 x = 0
- nsmul_succ (n : ℕ) (x : R) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- one : R
- natCast_zero : ↑0 = 0
- natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
- neg : R → R
- sub : R → R → R
- sub_eq_add_neg (a b : R) : a - b = a + -b
- zsmul : ℤ → R → R
- zsmul_zero' (a : R) : AddGroupWithOne.zsmul 0 a = 0
- zsmul_succ' (n : ℕ) (a : R) : AddGroupWithOne.zsmul (↑n.succ) a = AddGroupWithOne.zsmul (↑n) a + a
- zsmul_neg' (n : ℕ) (a : R) : AddGroupWithOne.zsmul (Int.negSucc n) a = -AddGroupWithOne.zsmul (↑n.succ) a
- neg_add_cancel (a : R) : -a + a = 0
- intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n

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

- intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)

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

Instances

source
class AddCommGroupWithOne (R : Type u) extends AddCommGroup R, AddGroupWithOne R, AddCommMonoidWithOne R :
Type u

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

- 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) : AddMonoid.nsmul 0 x = 0
- nsmul_succ (n : ℕ) (x : R) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
- neg : R → R
- sub : R → R → R
- sub_eq_add_neg (a b : R) : a - b = a + -b
- zsmul : ℤ → R → R
- zsmul_zero' (a : R) : SubNegMonoid.zsmul 0 a = 0
- zsmul_succ' (n : ℕ) (a : R) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
- zsmul_neg' (n : ℕ) (a : R) : SubNegMonoid.zsmul (Int.negSucc n) a = -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 : ↑0 = 0
- natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
- intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
- intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)

Instances