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 forInt.cast
.
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 #
- zsmul : ℤ → R → R
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
.
Instances
The canonical map
ℕ → R→ R
sends0 : ℕ
to0 : 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
.