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 , AddMonoidWithOne , AddGroup , NatCast , SubNegMonoid , AddMonoid , One , Neg , Sub , AddSemigroup , AddZeroClass , Zero , Add : Type u

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

theorem AddGroupWithOne.intCast_ofNat {R : Type u} [self : AddGroupWithOne R] (n : ℕ) : IntCast.intCast ↑n = ↑n

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

theorem AddGroupWithOne.intCast_negSucc {R : Type u} [self : AddGroupWithOne R] (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 , AddGroupWithOne , AddCommMonoidWithOne , IntCast , AddMonoidWithOne , AddGroup , AddCommMonoid , NatCast , SubNegMonoid , AddMonoid , One , Neg , Sub , AddCommSemigroup , AddSemigroup , AddZeroClass , Zero , AddCommMagma , Add : Type u

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