# The integers form a group #

This file contains the additive group and multiplicative monoid instances on the integers.

See note [foundational algebra order theory].

### Instances #

source
instance Int.instCommMonoid :
CommMonoid ℤ
Equations

- One or more equations did not get rendered due to their size.

source
instance Int.instAddCommGroup :
AddCommGroup ℤ
Equations

- One or more equations did not get rendered due to their size.

### Extra instances to short-circuit type class resolution #

These also prevent non-computable instances like `Int.instNormedCommRing` being used to construct these instances non-computably.

source
instance Int.instAddCommMonoid :
AddCommMonoid ℤ
Equations

- Int.instAddCommMonoid = inferInstance

source
instance Int.instAddMonoid :
AddMonoid ℤ
Equations

- Int.instAddMonoid = inferInstance

source
instance Int.instMonoid :
Monoid ℤ
Equations

- Int.instMonoid = inferInstance

source
instance Int.instCommSemigroup :
CommSemigroup ℤ
Equations

- Int.instCommSemigroup = inferInstance

source
instance Int.instSemigroup :
Semigroup ℤ
Equations

- Int.instSemigroup = inferInstance

source
instance Int.instAddGroup :
AddGroup ℤ
Equations

- Int.instAddGroup = inferInstance

source
instance Int.instAddCommSemigroup :
AddCommSemigroup ℤ
Equations

- Int.instAddCommSemigroup = inferInstance

source
instance Int.instAddSemigroup :
AddSemigroup ℤ
Equations

- Int.instAddSemigroup = inferInstance

source
@[simp]
theorem Int.nsmul_eq_mul (n : ℕ) (a : ℤ) :
n • a = ↑n * a
source
@[simp]
theorem Int.zsmul_eq_mul (n a : ℤ) :
n • a = n * a
source
theorem zsmul_int_int (a b : ℤ) :
a • b = a * b
source
theorem zsmul_int_one (n : ℤ) :
n • 1 = n