Documentation

Mathlib.Algebra.Group.Int

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 #

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
Equations
Equations

Miscellaneous lemmas #

theorem Int.toAdd_pow (a : Multiplicative ) (b : ) :
Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * b
theorem Int.toAdd_zpow (a : Multiplicative ) (b : ) :
Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * b
@[simp]
theorem Int.ofAdd_mul (a : ) (b : ) :
Multiplicative.ofAdd (a * b) = Multiplicative.ofAdd a ^ b

Units #

theorem Int.units_natAbs (u : ˣ) :
(u).natAbs = 1
@[simp]
theorem Int.natAbs_of_isUnit {u : } (hu : IsUnit u) :
u.natAbs = 1
theorem Int.isUnit_eq_one_or {u : } (hu : IsUnit u) :
u = 1 u = -1
theorem Int.isUnit_ne_iff_eq_neg {u : } {v : } (hu : IsUnit u) (hv : IsUnit v) :
u v u = -v
theorem Int.isUnit_eq_or_eq_neg {u : } {v : } (hu : IsUnit u) (hv : IsUnit v) :
u = v u = -v
theorem Int.isUnit_iff {u : } :
IsUnit 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 : } :
IsUnit u u.natAbs = 1
theorem Int.IsUnit.natAbs_eq {u : } :
IsUnit uu.natAbs = 1

Alias of the forward direction of Int.isUnit_iff_natAbs_eq.

theorem Int.isUnit_mul_self {u : } (hu : IsUnit u) :
u * u = 1
theorem Int.isUnit_add_isUnit_eq_isUnit_add_isUnit {a : } {b : } {c : } {d : } (ha : IsUnit a) (hb : IsUnit b) (hc : IsUnit c) (hd : IsUnit d) :
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