Documentation

Mathlib.Algebra.Group.Int.Defs

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_reducible]
instance Int.instCommMonoid :
CommMonoid ℤ
Equations
  • One or more equations did not get rendered due to their size.
source
@[instance_reducible]
instance Int.instAddCommGroup :
AddCommGroup ℤ
Equations
  • One or more equations did not get rendered due to their size.
source
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.

source
@[instance_reducible]
instance Int.instAddCommMonoid :
AddCommMonoid ℤ
Equations
source
@[instance_reducible]
instance Int.instAddMonoid :
AddMonoid ℤ
Equations
source
@[instance_reducible]
instance Int.instMonoid :
Monoid ℤ
Equations
source
@[instance_reducible]
instance Int.instCommSemigroup :
CommSemigroup ℤ
Equations
source
@[instance_reducible]
instance Int.instSemigroup :
Semigroup ℤ
Equations
source
@[instance_reducible]
instance Int.instAddGroup :
AddGroup ℤ
Equations
source
@[instance_reducible]
instance Int.instAddCommSemigroup :
AddCommSemigroup ℤ
Equations
source
@[instance_reducible]
instance Int.instAddSemigroup :
AddSemigroup ℤ
Equations
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
@[deprecated "use `zsmul_eq_mul`" (since := "2026-01-05")]
theorem zsmul_int_int (a b : ℤ) :
a • b = a * b
source
@[deprecated "use `zsmul_one`" (since := "2026-01-05")]
theorem zsmul_int_one (n : ℤ) :
n • 1 = n