# The integers form a group #

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

See note [foundational algebra order theory].

Equations
Equations

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

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

Equations
Equations
instance Int.instMonoid :
Equations
Equations
Equations
Equations
Equations
Equations

### Miscellaneous lemmas #

theorem Int.toAdd_pow (a : ) (b : ) :
theorem Int.toAdd_zpow (a : ) (b : ) :
@[simp]
theorem Int.ofAdd_mul (a : ) (b : ) :

### Units #

theorem Int.units_natAbs (u : ) :
(u).natAbs = 1
@[simp]
theorem Int.natAbs_of_isUnit {u : } (hu : ) :
u.natAbs = 1
theorem Int.isUnit_eq_one_or {u : } (hu : ) :
u = 1 u = -1
theorem Int.isUnit_ne_iff_eq_neg {u : } {v : } (hu : ) (hv : ) :
u v u = -v
theorem Int.isUnit_eq_or_eq_neg {u : } {v : } (hu : ) (hv : ) :
u = v u = -v
theorem Int.isUnit_iff {u : } :
u = 1 u = -1
theorem Int.eq_one_or_neg_one_of_mul_eq_one {u : } {v : } (h : u * v = 1) :
u = 1 u = -1
theorem Int.eq_one_or_neg_one_of_mul_eq_one' {u : } {v : } (h : u * v = 1) :
u = 1 v = 1 u = -1 v = -1
theorem Int.eq_of_mul_eq_one {u : } {v : } (h : u * v = 1) :
u = v
theorem Int.mul_eq_one_iff_eq_one_or_neg_one {u : } {v : } :
u * v = 1 u = 1 v = 1 u = -1 v = -1
theorem Int.eq_one_or_neg_one_of_mul_eq_neg_one' {u : } {v : } (h : u * v = -1) :
u = 1 v = -1 u = -1 v = 1
theorem Int.mul_eq_neg_one_iff_eq_one_or_neg_one {u : } {v : } :
u * v = -1 u = 1 v = -1 u = -1 v = 1
theorem Int.isUnit_iff_natAbs_eq {u : } :
u.natAbs = 1
theorem Int.IsUnit.natAbs_eq {u : } :
u.natAbs = 1

Alias of the forward direction of Int.isUnit_iff_natAbs_eq.

theorem Int.ofNat_isUnit {n : } :
IsUnit n
theorem Int.isUnit_mul_self {u : } (hu : ) :
u * u = 1
theorem Int.isUnit_add_isUnit_eq_isUnit_add_isUnit {a : } {b : } {c : } {d : } (ha : ) (hb : ) (hc : ) (hd : ) :
a + b = c + d a = c b = d a = d b = c
theorem Int.eq_one_or_neg_one_of_mul_eq_neg_one {u : } {v : } (h : u * v = -1) :
u = 1 u = -1
theorem zsmul_int_int (a : ) (b : ) :
a b = a * b
theorem zsmul_int_one (n : ) :
n 1 = n