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 #

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

Default value for IntCast.intCast in an AddGroupWithOne.


Additive groups with one #

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

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


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