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

instance Int.instCommMonoid : CommMonoid ℤ

instance Int.instAddCommGroup : AddCommGroup ℤ

instance Int.instIsAddTorsionFree : IsAddTorsionFree ℤ

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.

instance Int.instAddCommMonoid : AddCommMonoid ℤ

instance Int.instAddMonoid : AddMonoid ℤ

instance Int.instMonoid : Monoid ℤ

instance Int.instCommSemigroup : CommSemigroup ℤ

instance Int.instSemigroup : Semigroup ℤ

instance Int.instAddGroup : AddGroup ℤ

instance Int.instAddCommSemigroup : AddCommSemigroup ℤ

instance Int.instAddSemigroup : AddSemigroup ℤ

@[simp]

theorem Int.nsmul_eq_mul (n : ℕ) (a : ℤ) : n • a = ↑n * a

@[simp]

theorem Int.zsmul_eq_mul (n a : ℤ) : n • a = n * a

@[deprecated "use `zsmul_eq_mul`" (since := "2026-01-05")]

theorem zsmul_int_int (a b : ℤ) : a • b = a * b

@[deprecated "use `zsmul_one`" (since := "2026-01-05")]

theorem zsmul_int_one (n : ℤ) : n • 1 = n