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 forInt.cast
.
Default value for IntCast.intCast
in an AddGroupWithOne
.
Additive groups with one #
An AddGroupWithOne
is an AddGroup
with a 1. It also contains data for the unique
homomorphisms ℕ → R
and ℤ → R
.
- add : R → R → R
- zero : R
- one : R
- neg : R → R
- sub : R → R → R
- zsmul_neg' (n : ℕ) (a : R) : AddGroupWithOne.zsmul (Int.negSucc n) a = -AddGroupWithOne.zsmul (↑n.succ) a
The canonical homomorphism
ℤ → R
agrees with the one fromℕ → R
onℕ
.The canonical homomorphism
ℤ → R
for negative values is just the negation of the values of the canonical homomorphismℕ → R
.
Instances
- CauSeq.addGroupWithOne
- Complex.addGroupWithOne
- DirectLimit.instAddGroupWithOne
- Equiv.instAddGroupWithOneShrink
- Filter.Germ.instAddGroupWithOne
- Lex.instAddGroupWithOne
- Matrix.instAddGroupWithOne
- MulOpposite.instAddGroupWithOne
- OrderDual.instAddGroupWithOne
- Pi.addGroupWithOne
- Prod.instAddGroupWithOne
- ULift.addGroupWithOne
class
AddCommGroupWithOne
(R : Type u)
extends AddCommGroup R, AddGroupWithOne R, AddCommMonoidWithOne R :
Type u
An AddCommGroupWithOne
is an AddGroupWithOne
satisfying a + b = b + a
.
Instances
- AddOpposite.instAddCommGroupWithOne
- Algebra.TensorProduct.instAddCommGroupWithOne
- CommRing.toAddCommGroupWithOne
- DirectLimit.instAddCommGroupWithOneOfAddMonoidHomClass
- Lex.instAddCommGroupWithOne
- Matrix.instAddCommGroupWithOne
- MulOpposite.instAddCommGroupWithOne
- OrderDual.instAddCommGroupWithOne
- ULift.addCommGroupWithOne