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→ R field.

Preferentially, the homomorphism is written as a coercion.

Main declarations

• Int.cast: Canonical homomorphism ℤ → R→ R.
• AddGroupWithOne: Type class for Int.cast.

ink

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

Default value for IntCast.intCast in an AddGroupWithOne.

Equations

• Int.castDef x = match x with | Int.ofNat n => ↑n | Int.negSucc n => -↑(n + 1)

Additive groups with one

ink

class AddGroupWithOne (R : Type u) extends IntCast , AddMonoidWithOne , Neg , Sub : Type u

• sub_eq_add_neg : autoParam (∀ (a b : R), a - b = a + -b) _auto✝
• zsmul : ℤ → R → R
• zsmul_zero' : autoParam (∀ (a : R), zsmul 0 a = 0) _auto✝
• zsmul_succ' : autoParam (∀ (n : ℕ) (a : R), zsmul (Int.ofNat (Nat.succ n)) a = a + zsmul (Int.ofNat n) a) _auto✝
• zsmul_neg' : autoParam (∀ (n : ℕ) (a : R), zsmul (Int.negSucc n) a = -zsmul (↑(Nat.succ n)) a) _auto✝
• add_left_neg : ∀ (a : R), -a + a = 0

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

  intCast_ofNat : autoParam (∀ (n : ℕ), IntCast.intCast ↑n = ↑n) _auto✝

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

  intCast_negSucc : autoParam (∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)) _auto✝

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

ink

class AddCommGroupWithOne (R : Type u) extends AddCommGroup , IntCast , NatCast , One : Type u

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

  natCast_zero : autoParam (NatCast.natCast 0 = 0) _auto✝

• The canonical map ℕ → R→ R is a homomorphism.

  natCast_succ : autoParam (∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1) _auto✝

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

  intCast_ofNat : autoParam (∀ (n : ℕ), IntCast.intCast ↑n = ↑n) _auto✝

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

  intCast_negSucc : autoParam (∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)) _auto✝

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