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} [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)

Additive groups with one

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

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